isac-java/src/java-tests/isac/bridge/xml/TestsDATA.scala
changeset 5239 b4e3883d7b66
parent 5229 6bf0e95981e3
     1.1 --- a/isac-java/src/java-tests/isac/bridge/xml/TestsDATA.scala	Tue Sep 22 14:33:32 2020 +0200
     1.2 +++ b/isac-java/src/java-tests/isac/bridge/xml/TestsDATA.scala	Fri Mar 26 10:45:05 2021 +0100
     1.3 @@ -6,8 +6,8 @@
     1.4   */
     1.5  package isac.bridge.xml
     1.6  
     1.7 -import info.hupel.isabelle.api.XML
     1.8 -import info.hupel.isabelle.pure._ // DEFINES type Term
     1.9 +import edu.tum.cs.isabelle.api.XML
    1.10 +import edu.tum.cs.isabelle.pure._ // DEFINES type Term
    1.11  
    1.12  /*
    1.13   * Compile test data for TestDataTypes.java.
    1.14 @@ -114,4 +114,4 @@
    1.15    def term_mini_subpbl_1 (): Term = {
    1.16      App(Const("Equation.solve",Type("fun",List(Type("Product_Type.prod",List(Type("HOL.bool",List()), Type("Real.real",List()))), Type("List.list",List(Type("HOL.bool",List())))))),App(App(Const("Product_Type.Pair",Type("fun",List(Type("HOL.bool",List()), Type("fun",List(Type("Real.real",List()), Type("Product_Type.prod",List(Type("HOL.bool",List()), Type("Real.real",List())))))))),App(App(Const("HOL.eq",Type("fun",List(Type("Real.real",List()), Type("fun",List(Type("Real.real",List()), Type("HOL.bool",List())))))),App(App(Const("Groups.plus_class.plus",Type("fun",List(Type("Real.real",List()), Type("fun",List(Type("Real.real",List()), Type("Real.real",List())))))),Free("x",Type("Real.real",List()))),Free("1",Type("Real.real",List())))),Free("2",Type("Real.real",List())))),Free("x",Type("Real.real",List()))))
    1.17    }
    1.18 -}
    1.19 \ No newline at end of file
    1.20 +}