1.1 --- a/test/Tools/isac/Interpret/mathengine.sml Wed Feb 07 13:06:27 2018 +0100
1.2 +++ b/test/Tools/isac/Interpret/mathengine.sml Wed Feb 07 15:00:37 2018 +0100
1.3 @@ -624,9 +624,9 @@
1.4 BUT WE FIND IN THE CODE ABOVE IN next_tac:*)
1.5 ;
1.6 (*----------------------------------------------------------------------------------------------*)
1.7 -if string_of_thmI @{thm rnorm_equation_add} = "~ ?b =!= 0 ==> (?a = ?b) = (?a + - 1 * ?b = 0)"
1.8 +if string_of_thmI @{thm rnorm_equation_add} = "<not> ?b =!= 0 ==> (?a = ?b) = (?a + - 1 * ?b = 0)"
1.9 then () else error "string_of_thmI changed";
1.10 -if string_of_thm @{thm rnorm_equation_add} = "~ ?b =!= 0 ==> (?a = ?b) = (?a + - 1 * ?b = 0)"
1.11 +if string_of_thm @{thm rnorm_equation_add} = "<not> ?b =!= 0 ==> (?a = ?b) = (?a + - 1 * ?b = 0)"
1.12 then () else error "string_of_thm changed";
1.13 (*----------------------------------------------------------------------------------------------*)
1.14 ;
2.1 --- a/test/Tools/isac/Knowledge/partial_fractions.sml Wed Feb 07 13:06:27 2018 +0100
2.2 +++ b/test/Tools/isac/Knowledge/partial_fractions.sml Wed Feb 07 15:00:37 2018 +0100
2.3 @@ -247,7 +247,7 @@
2.4 terms2str' asms = "[~ matches (?a = 0) (3 = -3 * B / 4) | ~ lhs (3 = -3 * B / 4) is_poly_in B," ^
2.5 "B = -4,lhs (3 + 3 / 4 * B = 0) is_poly_in B,lhs (3 + 3 / 4 * B = 0) has_degree_in B = 1," ^
2.6 "B is_polyexp,A is_polyexp," ^
2.7 - "~ matches (?a = 0) (3 = 3 * A / 4) | ~ lhs (3 = 3 * A / 4) is_poly_in A," ^
2.8 + "<not> matches (?a = 0) (3 = 3 * A / 4) | <not> lhs (3 = 3 * A / 4) is_poly_in A," ^
2.9 "A = 4,lhs (3 + -3 / 4 * A = 0) is_poly_in A,lhs (3 + -3 / 4 * A = 0) has_degree_in A = 1," ^
2.10 "lhs (-1 + -2 * z + 8 * z ^^^ 2 = 0) has_degree_in z = 2," ^
2.11 "lhs (-1 + -2 * z + 8 * z ^^^ 2 = 0) is_poly_in z,z = 1 / 2,z = -1 / 4,z is_polyexp]"
3.1 --- a/test/Tools/isac/Knowledge/polyminus.sml Wed Feb 07 13:06:27 2018 +0100
3.2 +++ b/test/Tools/isac/Knowledge/polyminus.sml Wed Feb 07 15:00:37 2018 +0100
3.3 @@ -605,7 +605,7 @@
3.4 if term2str t = "~ (matchsub ((?a::real) + ((?b::real) + (?c::real))) (t_t::real) |\n matchsub (?a + (?b - ?c)) t_t |\n matchsub (?a - (?b + ?c)) t_t | matchsub (?a + (?b - ?c)) t_t)"
3.5 then () else error "polyminus.sml type-structure of \"?a :: real\" changed 1";
3.6 show_types := false;*)
3.7 -if term2str t = "~ (matchsub (?a + (?b + ?c)) t_t |\n matchsub (?a + (?b - ?c)) t_t |\n" ^
3.8 +if term2str t = "<not> (matchsub (?a + (?b + ?c)) t_t |\n matchsub (?a + (?b - ?c)) t_t |\n" ^
3.9 " matchsub (?a - (?b + ?c)) t_t | matchsub (?a + (?b - ?c)) t_t)"
3.10 then () else error "polyminus.sml type-structure of \"?a :: real\" changed 1";
3.11
4.1 --- a/test/Tools/isac/Knowledge/rateq.sml Wed Feb 07 13:06:27 2018 +0100
4.2 +++ b/test/Tools/isac/Knowledge/rateq.sml Wed Feb 07 15:00:37 2018 +0100
4.3 @@ -148,7 +148,7 @@
4.4
4.5 term2str bdv = "x";
4.6 terms2str asms = (* GOON: asms from rewriting are missing : vvv *)
4.7 - ("[\"~ matches (?a = 0) (1 = 5 * x) | ~ lhs (1 = 5 * x) is_poly_in x\",\"x = 1 / 5\"," ^
4.8 + ("[\"<not> matches (?a = 0) (1 = 5 * x) | ~ lhs (1 = 5 * x) is_poly_in x\",\"x = 1 / 5\"," ^
4.9 "\"lhs (1 + -5 * x = 0) is_poly_in x\",\"lhs (1 + -5 * x = 0) has_degree_in x = 1\"," ^
4.10 "\"1 / x = 5 is_ratequation_in x\"]");
4.11 (*
4.12 @@ -260,9 +260,9 @@
4.13 f2str f = "[x = 0, x = 6 / 5]"; (*= GUI*)
4.14 case snd nxt of Check_elementwise "Assumptions" => () | _ => ((*not checked before*)); (*= GUI*)
4.15 if terms2str (get_assumptions_ pt p) =
4.16 -("[\"~ matches (?a = 0)\n" ^
4.17 +("[\"<not> matches (?a = 0)\n" ^
4.18 " ((3 + -1 * x + x ^^^ 2) * x = 1 * (9 * x + -6 * x ^^^ 2 + x ^^^ 3)) |\n" ^
4.19 - "~ lhs ((3 + -1 * x + x ^^^ 2) * x =\n " ^
4.20 + "<not> lhs ((3 + -1 * x + x ^^^ 2) * x =\n " ^
4.21 " 1 * (9 * x + -6 * x ^^^ 2 + x ^^^ 3)) is_poly_in x\"," ^
4.22 "\"x = 6 / 5\"," ^
4.23 "\"x = 0\"," ^
5.1 --- a/test/Tools/isac/Minisubpbl/000-comments.sml Wed Feb 07 13:06:27 2018 +0100
5.2 +++ b/test/Tools/isac/Minisubpbl/000-comments.sml Wed Feb 07 15:00:37 2018 +0100
5.3 @@ -15,8 +15,8 @@
5.4 200 start and execute the method of the rootproblem
5.5 300 initialisation of a subproblem from script and specify phase
5.6 400 start and execute the method of the subproblem
5.7 - 490 last step of execution with next step Check_Postcond
5.8 + 490 last step of execution with next step Check_Postcond
5.9 500 shift interpretation from sub-method to root-method
5.10 - 550 found error in Check_Elementwise Assumptions
5.11 + 550 found error in Check_Elementwise Assumptions
5.12 600 check postconditions of subproblem and rootproblem
5.13 *)
6.1 --- a/test/Tools/isac/ProgLang/termC.sml Wed Feb 07 13:06:27 2018 +0100
6.2 +++ b/test/Tools/isac/ProgLang/termC.sml Wed Feb 07 15:00:37 2018 +0100
6.3 @@ -170,18 +170,18 @@
6.4 "----------- inst_bdv -----------------------------------";
6.5 "----------- inst_bdv -----------------------------------";
6.6 if (term2str o Thm.prop_of o num_str) @{thm d1_isolate_add2} =
6.7 - "~ ?bdv occurs_in ?a ==> (?a + ?bdv = 0) = (?bdv = -1 * ?a)"
6.8 + "\<not> ?bdv occurs_in ?a \<Longrightarrow>\n(?a + ?bdv = 0) = (?bdv = -1 * ?a)"
6.9 then ()
6.10 else error "termC.sml d1_isolate_add2";
6.11 val subst = [(str2term "bdv", str2term "x")];
6.12 val t = (norm o #prop o Thm.rep_thm) (num_str @{thm d1_isolate_add2});
6.13 val t' = inst_bdv subst t;
6.14 - if term2str t' = "~ x occurs_in ?a ==> (?a + x = 0) = (x = -1 * ?a)"
6.15 + if term2str t' = "\<not> x occurs_in ?a \<Longrightarrow> (?a + x = 0) = (x = -1 * ?a)"
6.16 then ()
6.17 else error "termC.sml inst_bdv 1";
6.18 if (term2str o Thm.prop_of o num_str) @{thm separate_bdvs_add} =
6.19 - "[] from [?bdv_1.0, ?bdv_2.0, ?bdv_3.0, ?bdv_4.0] occur_exactly_in ?a\n==>" ^
6.20 - " (?a + ?b = ?c) = (?b = ?c + -1 * ?a)"
6.21 + "[] from [?bdv_1.0, ?bdv_2.0, ?bdv_3.0,\n "
6.22 + ^ "?bdv_4.0] occur_exactly_in ?a \<Longrightarrow>\n(?a + ?b = ?c) = (?b = ?c + -1 * ?a)"
6.23 then () else error "termC.sml separate_bdvs_add";
6.24 (*default_print_depth 5;*)
6.25
6.26 @@ -193,8 +193,8 @@
6.27 val t = (norm o #prop o Thm.rep_thm) (num_str @{thm separate_bdvs_add});
6.28 val t' = inst_bdv subst t;
6.29
6.30 -if term2str t' = "[] from [c, c_2, c_3, c_4] occur_exactly_in ?a\n\
6.31 - \==> (?a + ?b = ?c) = (?b = ?c + -1 * ?a)"
6.32 +if term2str t' = "[] from [c, c_2, c_3, c_4] occur_exactly_in ?a \<Longrightarrow>\n"
6.33 + ^ "(?a + ?b = ?c) = (?b = ?c + -1 * ?a)"
6.34 then () else error "termC.sml inst_bdv 2";
6.35
6.36 "----------- subst_atomic_all ---------------------------";
6.37 @@ -424,16 +424,17 @@
6.38 |> numbers_to_string;
6.39 val t_real = typ_a2real t;
6.40 if term_to_string' ctxt t_real =
6.41 -"~ (matchsub ((?a::real) + ((?b::real) + (?c::real))) (t_t::real) |\n matchsub (?a + (?b - ?c))" ^
6.42 -" t_t |\n matchsub (?a - (?b + ?c)) t_t | matchsub (?a + (?b - ?c)) t_t)" then ()
6.43 -else error "";
6.44 + "\<not> (matchsub ((?a::real) + ((?b::real) + (?c::real))) (t_t::real) \<or>\n "
6.45 + ^ "matchsub (?a + (?b - ?c)) t_t \<or>\n "
6.46 + ^ "matchsub (?a - (?b + ?c)) t_t \<or> matchsub (?a + (?b - ?c)) t_t)" then ()
6.47 +else error "matchsub";
6.48
6.49 "----------- check writeln, tracing for string markup ---";
6.50 "----------- check writeln, tracing for string markup ---";
6.51 "----------- check writeln, tracing for string markup ---";
6.52 val t = @{term "x + 1"};
6.53 val str_markup = (Syntax.string_of_term
6.54 - (Proof_Context.init_global (Thy_Info.get_theory "Isac"))) t;
6.55 + (Proof_Context.init_global (Thy_Info_get_theory "Isac"))) t;
6.56 val str = term_to_string'' "Isac" t;
6.57
6.58 writeln "----------------writeln str_markup---";
6.59 @@ -471,7 +472,7 @@
6.60 "----------- check writeln, tracing for string markup ---";
6.61 val t = @{term "x + 1"};
6.62 val str_markup = (Syntax.string_of_term
6.63 - (Proof_Context.init_global (Thy_Info.get_theory "Isac"))) t;
6.64 + (Proof_Context.init_global (Thy_Info_get_theory "Isac"))) t;
6.65 val str = term_to_string'' "Isac" t;
6.66
6.67 writeln "----------------writeln str_markup---";
7.1 --- a/test/Tools/isac/Test_Isac.thy Wed Feb 07 13:06:27 2018 +0100
7.2 +++ b/test/Tools/isac/Test_Isac.thy Wed Feb 07 15:00:37 2018 +0100
7.3 @@ -121,12 +121,12 @@
7.4 (*---------------------- do Minisubpbl before ADDTESTS/All_Ctxt --------------------------------
7.5 ML_file "kestore.sml" (* setup in ADDTEST/accumulate-val/lucas_interpreter.sml*)
7.6 ---------------------- do Minisubpbl before ADDTESTS/All_Ctxt --------------------------------*)
7.7 + ML_file "ProgLang/termC.sml"
7.8 ML {*
7.9 *} ML {*
7.10 *} ML {*
7.11 *}
7.12 (*---------------------- do Minisubpbl before ADDTESTS/All_Ctxt --------------------------------
7.13 - ML_file "ProgLang/termC.sml"
7.14 ML_file "ProgLang/calculate.sml" (* requires setup from calculate.thy *)
7.15 ML_file "ProgLang/rewrite.sml"
7.16 ML_file "ProgLang/listC.sml"