1.1 --- a/isac-java/src/java-tests/isac/gui/mawen/TestUseCases.scala	Thu Jul 06 14:15:34 2017 +0200
     1.2 +++ b/isac-java/src/java-tests/isac/gui/mawen/TestUseCases.scala	Thu Jul 06 15:36:25 2017 +0200
     1.3 @@ -55,6 +55,26 @@
     1.4                Variable("2"))))))))))
     1.5      //println(Ast.math_string_of(ast))
     1.6      assertEquals(math_string_of(ast), term_str)
     1.7 +    val ast_05 =
     1.8 +      Appl(List(
     1.9 +        Constant("Groups.plus_class.plus"),
    1.10 +        Appl(List(
    1.11 +          Constant("Diff.d_d"),
    1.12 +          Variable("x"),
    1.13 +          Variable("x"))),
    1.14 +        Appl(List(
    1.15 +          Constant("Diff.d_d"),
    1.16 +          Variable("x"),
    1.17 +          Appl(List(                 //added to above
    1.18 +            Constant("BOX.1"),       //added to above
    1.19 +            Appl(List(
    1.20 +              Constant("Transcendental.sin"),
    1.21 +              Appl(List(             //added to above
    1.22 +                Constant("BOX.2"),   //added to above
    1.23 +                Appl(List(
    1.24 +                  Constant("Power.power_class.power"),
    1.25 +                  Variable("x"),
    1.26 +                  Variable("2")))))))))))))
    1.27  
    1.28      term_str = "d_d bdv (sin (u)) = cos (u) * d_d bdv u"
    1.29      tree = sys_.invoke(isac.bridge.IsacOperations.SCALATERM_OF_STRING, term_str)
    1.30 @@ -81,6 +101,32 @@
    1.31              Variable("u"))))))))
    1.32      //println(Ast.math_string_of(ast))
    1.33      assertEquals(math_string_of(ast), term_str)
    1.34 +    val ast_06 =
    1.35 +      Appl(List(
    1.36 +        Constant("HOL.eq"),
    1.37 +        Appl(List(
    1.38 +          Constant("Diff.d_d"),
    1.39 +          Variable("bdv"),
    1.40 +          Appl(List(                 //added to above
    1.41 +            Constant("BOX.1"),       //added to above
    1.42 +            Appl(List(
    1.43 +              Constant("Transcendental.sin"),
    1.44 +              Appl(List(             //added to above
    1.45 +                Constant("BOX.2"),   //added to above
    1.46 +                Variable("u"))))))))),
    1.47 +        Appl(List(
    1.48 +          Constant("Groups.times_class.times"),
    1.49 +          Appl(List(                 //added to above
    1.50 +            Constant("BOX.3"),       //added to above
    1.51 +            Appl(List(
    1.52 +              Constant("Transcendental.cos"),
    1.53 +              Variable("u"))))),
    1.54 +          Appl(List(
    1.55 +            Constant("Diff.d_d"),
    1.56 +            Variable("bdv"),
    1.57 +            Appl(List(               //added to above
    1.58 +              Constant("BOX.4"),     //added to above
    1.59 +              Variable("u")))))))))
    1.60      
    1.61      term_str = "d_d x x + cos (x ^ 2) * d_d x GAP"
    1.62      tree = sys_.invoke(isac.bridge.IsacOperations.SCALATERM_OF_STRING, term_str)
    1.63 @@ -108,6 +154,29 @@
    1.64              Variable("GAP")))))))) //NOT Constant("#"), because comes from Isabelle_Isac
    1.65      //println(Ast.math_string_of(ast))
    1.66      assertEquals(math_string_of(ast), term_str) //Isabelle requires (sin (x ^ 2)
    1.67 +    val ast_07 =
    1.68 +      Appl(List(
    1.69 +        Constant("Groups.plus_class.plus"),
    1.70 +        Appl(List(
    1.71 +          Constant("Diff.d_d"),
    1.72 +          Variable("x"),
    1.73 +          Variable("x"))),
    1.74 +        Appl(List(
    1.75 +          Constant("Groups.times_class.times"),
    1.76 +          Appl(List(                 //added to above
    1.77 +            Constant("BOX.3"),       //added to above
    1.78 +            Appl(List(
    1.79 +              Constant("Transcendental.cos"),
    1.80 +              Appl(List(
    1.81 +                Constant("Power.power_class.power"),
    1.82 +                Variable("x"),
    1.83 +                Variable("2"))))))),
    1.84 +          Appl(List(
    1.85 +            Constant("Diff.d_d"),
    1.86 +            Variable("x"),
    1.87 +            Appl(List(               //added to above
    1.88 +              Constant("BOX.4"),     //added to above
    1.89 +              Variable("GAP")))))))))
    1.90       
    1.91      println("\\--END isac.gui.mawen.TestUseCases#testUC_userguide");
    1.92    }