1.1 --- a/src/Tools/isac/Interpret/appl.sml Thu Mar 10 15:19:26 2011 +0100
1.2 +++ b/src/Tools/isac/Interpret/appl.sml Thu Mar 10 16:04:00 2011 +0100
1.3 @@ -165,12 +165,12 @@
1.4 > val ct = "((#0 <= #18 & #0 <= sqrt (#5 + #3) + sqrt (#5 - #3)) &\
1.5 \ #0 <= #25 + #-1 * #3 ^^^ #2) & #0 <= #4";
1.6 > val SOME(ct',_) = rewrite_set "Isac" false "eval_rls" ct;
1.7 -val ct' = "True" : cterm'
1.8 +val ct' = "HOL.True" : cterm'
1.9
1.10 > val ct = "((#0 <= #18 & #0 <= sqrt (#5 + #-3) + sqrt (#5 - #-3)) &\
1.11 \ #0 <= #25 + #-1 * #-3 ^^^ #2) & #0 <= #4";
1.12 > val SOME(ct',_) = rewrite_set "Isac" false "eval_rls" ct;
1.13 -val ct' = "True" : cterm'
1.14 +val ct' = "HOL.True" : cterm'
1.15
1.16
1.17 > val const = (term_of o the o (parse thy)) "(#3::real)";
2.1 --- a/src/Tools/isac/Interpret/script.sml Thu Mar 10 15:19:26 2011 +0100
2.2 +++ b/src/Tools/isac/Interpret/script.sml Thu Mar 10 16:04:00 2011 +0100
2.3 @@ -153,7 +153,7 @@
2.4 > get [] (eq_str "Let") sss; [R]
2.5 > get [] (eq_str "Script.Try") sss; [R,L,R]
2.6 > get [] (eq_str "Script.Rewrite") sss; [R,L,R,R]
2.7 -> get [] (eq_str "True") sss; [R,L,R,R,L,R]
2.8 +> get [] (eq_str "HOL.True") sss; [R,L,R,R,L,R]
2.9 > get [] (eq_str "e_") sss; [R,R]
2.10 *)
2.11
3.1 --- a/src/Tools/isac/Knowledge/Atools.thy Thu Mar 10 15:19:26 2011 +0100
3.2 +++ b/src/Tools/isac/Knowledge/Atools.thy Thu Mar 10 16:04:00 2011 +0100
3.3 @@ -322,7 +322,7 @@
3.4 > val t = str2term "0 = 0";
3.5 > val SOME (t',_) = rewrite_ thy dummy_ord e_rls false reflI t;
3.6 > term2str t';
3.7 -val it = "True"
3.8 +val it = "HOL.True"
3.9
3.10 val t = str2term "Not (x = 0)";
3.11 atomt t; term2str t;
4.1 --- a/src/Tools/isac/Knowledge/DiophantEq.thy Thu Mar 10 15:19:26 2011 +0100
4.2 +++ b/src/Tools/isac/Knowledge/DiophantEq.thy Thu Mar 10 16:04:00 2011 +0100
4.3 @@ -33,7 +33,7 @@
4.4 ML {*
4.5 val subst = [(parseNEW ctxt "bdv::int", parseNEW ctxt "x::int")];
4.6 val t = parseNEW ctxt "x + 1 = (2::int)";
4.7 -*}
4.8 +*}
4.9
4.10 ML {*
4.11 rewrite_inst_ thy e_rew_ord e_rls true subst (@{thm "int_isolate_add"}) t;
5.1 --- a/src/Tools/isac/Knowledge/LinEq.thy Thu Mar 10 15:19:26 2011 +0100
5.2 +++ b/src/Tools/isac/Knowledge/LinEq.thy Thu Mar 10 16:04:00 2011 +0100
5.3 @@ -129,7 +129,7 @@
5.4 (prep_pbt thy "pbl_equ_univ_lin" [] e_pblID
5.5 (["linear","univariate","equation"],
5.6 [("#Given" ,["equality e_e","solveFor v_v"]),
5.7 - ("#Where" ,["False", (*WN0509 just detected: this pbl can never be used?!?*)
5.8 + ("#Where" ,["HOL.False", (*WN0509 just detected: this pbl can never be used?!?*)
5.9 "Not( (lhs e_e) is_polyrat_in v_v)",
5.10 "Not( (rhs e_e) is_polyrat_in v_v)",
5.11 "((lhs e_e) has_degree_in v_v)=1",
6.1 --- a/src/Tools/isac/Knowledge/Test.thy Thu Mar 10 15:19:26 2011 +0100
6.2 +++ b/src/Tools/isac/Knowledge/Test.thy Thu Mar 10 16:04:00 2011 +0100
6.3 @@ -806,7 +806,7 @@
6.4 > val SOME (ct,_) = rewrite_ thy sqrt_right tval_rls false or_false ct;
6.5 > val SOME (ct,_) = rewrite_ thy sqrt_right tval_rls false or_false ct;
6.6 > val SOME (ct,_) = rewrite_ thy sqrt_right tval_rls false or_false ct;
6.7 -val ct = "True" : cterm
6.8 +val ct = "HOL.True" : cterm
6.9
6.10 *)
6.11
6.12 @@ -816,7 +816,7 @@
6.13 (prep_pbt thy "pbl_test_uni_poly" [] e_pblID
6.14 (["polynomial","univariate","equation","test"],
6.15 [("#Given" ,["equality (v_v ^^^2 + p_p * v_v + q__q = 0)","solveFor v_v"]),
6.16 - ("#Where" ,["False"]),
6.17 + ("#Where" ,["HOL.False"]),
6.18 ("#Find" ,["solutions v_v'i'"])
6.19 ],
6.20 e_rls, SOME "solve (e_e::bool, v_v)", []));
7.1 --- a/src/Tools/isac/ProgLang/Tools.thy Thu Mar 10 15:19:26 2011 +0100
7.2 +++ b/src/Tools/isac/ProgLang/Tools.thy Thu Mar 10 16:04:00 2011 +0100
7.3 @@ -58,8 +58,8 @@
7.4 val EmptyList = (term_of o the o (parse @{theory})) "[]::bool list";
7.5
7.6 (*+ for Or_to_List +*)
7.7 -fun or2list (Const ("True",_)) = (tracing"### or2list True";UniversalList)
7.8 - | or2list (Const ("False",_)) = (tracing"### or2list False";EmptyList)
7.9 +fun or2list (Const ("HOL.True",_)) = (tracing"### or2list True";UniversalList)
7.10 + | or2list (Const ("HOL.False",_)) = (tracing"### or2list False";EmptyList)
7.11 | or2list (t as Const ("HOL.eq",_) $ _ $ _) =
7.12 (tracing"### or2list _ = _";list2isalist bool [t])
7.13 | or2list ors =
8.1 --- a/src/Tools/isac/ProgLang/calculate.sml Thu Mar 10 15:19:26 2011 +0100
8.2 +++ b/src/Tools/isac/ProgLang/calculate.sml Thu Mar 10 16:04:00 2011 +0100
8.3 @@ -330,7 +330,7 @@
8.4 > val ct = (the o (parse thy)) "~ ( 4 + (4 * x + x ^ 2) =!= (+0))";
8.5 > val rls = eval_rls;
8.6 > val (ct,_) = the (rewrite_set_ thy false rls ct);
8.7 -val ct = "True" : cterm
8.8 +val ct = "HOL.True" : cterm
8.9 --------------------------
8.10 *)
8.11
9.1 --- a/src/Tools/isac/ProgLang/rewrite.sml Thu Mar 10 15:19:26 2011 +0100
9.2 +++ b/src/Tools/isac/ProgLang/rewrite.sml Thu Mar 10 16:04:00 2011 +0100
9.3 @@ -22,9 +22,9 @@
9.4 else NONE end)
9.5 (* one rewrite (possibly conditional, ordered) EXOR exn EXOR go into subterms *)
9.6 and rew_sub thy i bdv tless rls put_asm lrd r t =
9.7 - (tracing ("@@@ rew_sub begin: t = "^(term2str t));
9.8 + ((*tracing ("@@@ rew_sub begin: t = "^(term2str t));
9.9 tracing ("@@@ rew_sub begin: bdv = "^(PolyML.makestring bdv));
9.10 - tracing ("@@@ rew_sub begin: r = "^(term2str r));
9.11 + tracing ("@@@ rew_sub begin: r = "^(term2str r));*)
9.12 let (* copy from Pure/thm.ML: fun rewritec *)
9.13 val (lhs, rhs) = (HOLogic.dest_eq o HOLogic.dest_Trueprop
9.14 o Logic.strip_imp_concl) r;
9.15 @@ -617,20 +617,20 @@
9.16
9.17
9.18 (*vor check_elementwise: SqRoot_eval_rls .. wie *_simplify ?! TODO *)
9.19 -fun eval_true' (thy':theory') (rls':rls') (Const ("True",_)) = true
9.20 +fun eval_true' (thy':theory') (rls':rls') (Const ("HOL.True",_)) = true
9.21
9.22 | eval_true' (thy':theory') (rls':rls') (t:term) =
9.23 (* val thy'="Isac"; val rls'="eval_rls"; val t=hd pres';
9.24 *)
9.25 let val ct' = term2str t;
9.26 in case rewrite_set thy' false rls' ct' of
9.27 - SOME ("True",_) => true
9.28 + SOME ("HOL.True",_) => true
9.29 | _ => false
9.30 end;
9.31 -fun eval_true_ _ _ (Const ("True",_)) = true
9.32 +fun eval_true_ _ _ (Const ("HOL.True",_)) = true
9.33 | eval_true_ (thy':theory') rls t =
9.34 case rewrite_set_ (assoc_thy thy') false rls t of
9.35 - SOME (Const ("True",_),_) => true
9.36 + SOME (Const ("HOL.True",_),_) => true
9.37 | _ => false;
9.38
9.39 (*
9.40 @@ -656,7 +656,7 @@
9.41
9.42 rewrite_set_ (Thy_Info.get_theory "Isac") eval_rls false eval_rls
9.43 ((the o (parse thy)) "contains_root (sqrt #0)");
9.44 -val it = SOME ("True",[]) : (cterm * cterm list) option
9.45 +val it = SOME ("HOL.True",[]) : (cterm * cterm list) option
9.46
9.47 *)
9.48
9.49 @@ -678,8 +678,8 @@
9.50 determine dts;
9.51 val it =
9.52 (FALSE,
9.53 - [Const ("empty","'a"),Const ("False","bool"),Const ("empty","'a"),
9.54 - Const ("True","bool")]) : det * term list*)
9.55 + [Const ("empty","'a"),Const ("HOL.False","bool"),Const ("empty","'a"),
9.56 + Const ("HOL.True","bool")]) : det * term list*)
9.57
9.58 fun eval__indet_ thy cs rls = (*FIXXME.WN:16.5.03 pull into eval__true_, update check (check_elementwise), and regard eval_true_ + eval_true*)
9.59 if cs = [HOLogic.true_const] orelse cs = [] then (TRUE, [])
10.1 --- a/src/Tools/isac/Test_Isac.thy Thu Mar 10 15:19:26 2011 +0100
10.2 +++ b/src/Tools/isac/Test_Isac.thy Thu Mar 10 16:04:00 2011 +0100
10.3 @@ -39,145 +39,6 @@
10.4 *)
10.5 use"../../../test/Tools/isac/ProgLang/termC.sml" (*part.*)
10.6 use"../../../test/Tools/isac/ProgLang/calculate.sml" (*part.*)
10.7 -
10.8 -ML {*
10.9 -"----------- assemble rewrite ---------------------------";
10.10 -"===== rewriting by thm with 'a";
10.11 -(*show_types := true;*)
10.12 -val thy = @{theory Complex_Main};
10.13 -val ctxt = @{context};
10.14 -val thm = @{thm add_commute};
10.15 -val t = (term_of o the) (parse thy "((r + u) + t) + s");
10.16 -"----- from old: fun rewrite__";
10.17 -val bdv = [];
10.18 -*}
10.19 -ML {*
10.20 -val r = (((inst_bdv bdv) o norm o #prop o rep_thm) thm);
10.21 -term2str r;
10.22 -*}
10.23 -
10.24 -ML {* (*TermC.sml*)
10.25 -
10.26 -*}
10.27 -
10.28 -ML {*
10.29 -"--------------------------------------------------------";
10.30 -val thy = @{theory Complex_Main};
10.31 -val thm = @{thm add_commute};
10.32 -val rule = (#prop o rep_thm) thm;
10.33 -"--------------------------------------------------------";
10.34 -term2str rule;
10.35 -
10.36 - val (prems,concl)=(map strip_trueprop(Logic.strip_imp_prems rule),
10.37 - (strip_trueprop o Logic.strip_imp_concl)rule);
10.38 -"--------------------------------------------------------";
10.39 -concl;
10.40 - is_equality concl; (*Isabelle2009-2: true, Isabelle2011: false*)
10.41 -(*-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.
10.42 -val (l,r) = dest_equals' concl;
10.43 - l = r; (*Isabelle2009-2: false*)
10.44 -
10.45 -val rule' = norm rule;
10.46 -rule = rule'; (*Isabelle2009-2: true*)
10.47 -term2str rule';
10.48 -(*Isabelle2009-2: val it = "?a + ?b = ?b + ?a" : string*)
10.49 -(*Isabelle2011: val it = "(?a + ?b = ?b + ?a) = True": string*)
10.50 --.-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.*)
10.51 -*}
10.52 -
10.53 -ML {*Trueprop*}
10.54 -
10.55 -ML {*
10.56 -
10.57 -Config.put show_types true (thy2ctxt (@{theory "Isac"}))
10.58 -
10.59 -*}
10.60 -
10.61 -ML {*
10.62 -"----- from old: and rew_sub";
10.63 -val (lhs,rhs) = (dest_equals' o strip_trueprop
10.64 - o Logic.strip_imp_concl) r;
10.65 -*}
10.66 -ML {*
10.67 -(* old
10.68 -val insts = Pattern.match thy (lhs,t) (Vartab.empty, Vartab.empty);*)
10.69 -"----- fun match_rew in Pure/pattern.ML";
10.70 -val rtm = the_default rhs (Term.rename_abs lhs t rhs);
10.71 -*}
10.72 -ML {*
10.73 -
10.74 -writeln(Syntax.string_of_term ctxt rtm);
10.75 -writeln(Syntax.string_of_term ctxt lhs);
10.76 -writeln(Syntax.string_of_term ctxt t);
10.77 -
10.78 -(Pattern.match thy (lhs, t) (Vartab.empty, Vartab.empty));
10.79 -*}
10.80 -ML {*
10.81 -val (rew, rhs) = (Envir.subst_term
10.82 - (Pattern.match thy (lhs, t) (Vartab.empty, Vartab.empty)) rtm, rtm);
10.83 -(*lookup in isabelle?trace?response...*)
10.84 -writeln(Syntax.string_of_term ctxt rew);
10.85 -writeln(Syntax.string_of_term ctxt rhs);
10.86 -
10.87 -*}
10.88 -ML {*
10.89 -"===== rewriting: prep insertion into rew_sub";
10.90 -val thy = @{theory Complex_Main};
10.91 -val ctxt = @{context};
10.92 -val thm = @{thm nonzero_mult_divide_cancel_right};
10.93 -val r = Thm.prop_of thm;"----------- assemble rewrite ---------------------------";
10.94 -"===== rewriting by thm with 'a";
10.95 -show_types := true;
10.96 -val thy = @{theory Complex_Main};
10.97 -val ctxt = @{context};
10.98 -val thm = @{thm add_commute};
10.99 -val t = (term_of o the) (parse thy "((r + u) + t) + s");
10.100 -"----- from old: fun rewrite__";
10.101 -val bdv = [];
10.102 -val r = (((inst_bdv bdv) o norm o #prop o rep_thm) thm);
10.103 -"----- from old: and rew_sub";
10.104 -val (lhs,rhs) = (dest_equals' o strip_trueprop
10.105 - o Logic.strip_imp_concl) r;
10.106 -(* old
10.107 -val insts = Pattern.match thy (lhs,t) (Vartab.empty, Vartab.empty);*)
10.108 -"----- fun match_rew in Pure/pattern.ML";
10.109 -val rtm = the_default rhs (Term.rename_abs lhs t rhs);
10.110 -
10.111 -writeln(Syntax.string_of_term ctxt rtm);
10.112 -writeln(Syntax.string_of_term ctxt lhs);
10.113 -writeln(Syntax.string_of_term ctxt t);
10.114 -
10.115 -(Pattern.match thy (lhs, t) (Vartab.empty, Vartab.empty));
10.116 -val (rew, rhs) = (Envir.subst_term
10.117 - (Pattern.match thy (lhs, t) (Vartab.empty, Vartab.empty)) rtm, rtm);
10.118 -(*lookup in isabelle?trace?response...*)
10.119 -writeln(Syntax.string_of_term ctxt rew);
10.120 -writeln(Syntax.string_of_term ctxt rhs);
10.121 -
10.122 -"===== rewriting: prep insertion into rew_sub";
10.123 -val thy = @{theory Complex_Main};
10.124 -val ctxt = @{context};
10.125 -val thm = @{thm nonzero_mult_divide_cancel_right};
10.126 -val r = Thm.prop_of thm;
10.127 -val tm = @{term "x*2 / 2::real"};
10.128 -"----- and rew_sub";
10.129 -val (lhs, rhs) = (HOLogic.dest_eq o HOLogic.dest_Trueprop
10.130 - o Logic.strip_imp_concl) r;
10.131 -val r' = Envir.subst_term (Pattern.match thy (lhs, tm)
10.132 - (Vartab.empty, Vartab.empty)) r;
10.133 -val p' = (fst o Logic.strip_prems) (Logic.count_prems r', [], r');
10.134 -val t' = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop
10.135 - o Logic.strip_imp_concl) r';
10.136 -
10.137 -(*is displayed on top of <response> buffer...*)
10.138 -Pretty.writeln (ProofContext.pretty_term_abbrev @{context} r');
10.139 -Pretty.writeln (ProofContext.pretty_term_abbrev @{context} t');
10.140 -(*}*)
10.141 -
10.142 -"----------- test rewriting without Isac's thys ---------";
10.143 -*}
10.144 -
10.145 -
10.146 use"../../../test/Tools/isac/ProgLang/rewrite.sml" (*GOON*)
10.147 (*
10.148 use"listg.sml";
10.149 @@ -186,29 +47,29 @@
10.150 cd "../..";
10.151 cd"smltest/ME";
10.152 *)
10.153 -use "../../../test/Tools/isac/Interpret/mstools.sml"; (*empty*)
10.154 +use "../../../test/Tools/isac/Interpret/mstools.sml" (*empty*)
10.155 (* use"ctree.sml";
10.156 *)
10.157 -use "../../../test/Tools/isac/Interpret/ptyps.sml"; (*TODO*)
10.158 -use "../../../test/Tools/isac/Interpret/calchead.sml";
10.159 +use "../../../test/Tools/isac/Interpret/ptyps.sml" (*TODO*)
10.160 +use "../../../test/Tools/isac/Interpret/calchead.sml"
10.161 ML {*print_depth 999*}
10.162 -use "../../../test/Tools/isac/Interpret/rewtools.sml"; (**)
10.163 +use "../../../test/Tools/isac/Interpret/rewtools.sml" (**)
10.164 (*
10.165 use"solve.sml"; (*detailrls can notyet ackn. 'Rewrite_Set "cancel"' *);
10.166 use"inform.sml";
10.167 *)
10.168 ML {*print_depth 5*}
10.169 -use "../../../test/Tools/isac/Interpret/mathengine.sml"; (*part.*)
10.170 +use "../../../test/Tools/isac/Interpret/mathengine.sml" (*part.*)
10.171 (*
10.172 use"me.sml";
10.173 cd "../..";
10.174 cd"smltest/xmlsrc";
10.175 use"datatypes.sml";
10.176 use"pbl-met-hierarchy.sml";
10.177 -use"../../../test/Tools/isac/xmlsrc/thy-hierarchy.sml"; (**)
10.178 +use"../../../test/Tools/isac/xmlsrc/thy-hierarchy.sml" (**)
10.179 *)
10.180
10.181 -use"../../../test/Tools/isac/Frontend/interface.sml"; (**)
10.182 +use"../../../test/Tools/isac/Frontend/interface.sml" (**)
10.183 (*
10.184 cd "../..";
10.185 *)
10.186 @@ -222,16 +83,16 @@
10.187 print_depth 999
10.188 *}
10.189 ML {*print_depth 5*}
10.190 -use"../../../test/Tools/isac/Knowledge/simplify.sml"; (*part.*)
10.191 +use"../../../test/Tools/isac/Knowledge/simplify.sml" (*part.*)
10.192 (*
10.193 use"poly.sml"
10.194 *)
10.195 -use"../../../test/Tools/isac/Knowledge/rational.sml"; (*part.*)
10.196 +use"../../../test/Tools/isac/Knowledge/rational.sml" (*part.*)
10.197 (*
10.198 use"equation.sml";
10.199 use"root.sml";
10.200 *)
10.201 -use "../../../test/Tools/isac/Knowledge/inssort.sml"; (*part.*)
10.202 +use "../../../test/Tools/isac/Knowledge/inssort.sml" (*part.*)
10.203 (*
10.204 (*use"inssort.sml"; problems with recdef in Isabelle2002*)
10.205 use"rooteq.sml";
10.206 @@ -248,13 +109,13 @@
10.207 use"logexp.sml";
10.208 *)
10.209 ML {*print_depth 5*}
10.210 -use "../../../test/Tools/isac/Knowledge/diff.sml"; (* *)
10.211 -use "../../../test/Tools/isac/Knowledge/integrate.sml"; (*complete*)
10.212 +use "../../../test/Tools/isac/Knowledge/diff.sml" (* *)
10.213 +use "../../../test/Tools/isac/Knowledge/integrate.sml" (*complete*)
10.214 (*
10.215 use"eqsystem.sml";
10.216 *)
10.217 ML {*print_depth 5*}
10.218 -use "../../../test/Tools/isac/Knowledge/polyminus.sml"; (* part. *)
10.219 +use "../../../test/Tools/isac/Knowledge/polyminus.sml" (* part. *)
10.220 (*
10.221 use"vect.sml";
10.222 use"diffapp.sml";
10.223 @@ -264,7 +125,7 @@
10.224 ML {*
10.225 Thy_Info.get_theory "Isac"
10.226 *}
10.227 -use "../../../test/Tools/isac/Knowledge/isac.sml"; (**)
10.228 +use "../../../test/Tools/isac/Knowledge/isac.sml" (**)
10.229
10.230 ML {*print_depth 3*}
10.231 ML {*111*}
11.1 --- a/test/Tools/isac/Knowledge/diffapp.sml Thu Mar 10 15:19:26 2011 +0100
11.2 +++ b/test/Tools/isac/Knowledge/diffapp.sml Thu Mar 10 16:04:00 2011 +0100
11.3 @@ -488,7 +488,7 @@
11.4 "1 < length_ [A = a * b, (a / 2) ^^^ 2 + (b / 2) ^^^ 2 = r ^^^ 2]";
11.5 val SOME (s',_) = rewrite_set_ thy false list_rls s;
11.6 val s'' = term2str s';
11.7 -if s''="True" then () else error "new behaviour with list_rls 1.2.";
11.8 +if s''="HOL.True" then () else error "new behaviour with list_rls 1.2.";
11.9
11.10 (*--- 2.line in script ---*)
11.11 val t = str2term
12.1 --- a/test/Tools/isac/Knowledge/eqsystem.sml Thu Mar 10 15:19:26 2011 +0100
12.2 +++ b/test/Tools/isac/Knowledge/eqsystem.sml Thu Mar 10 16:04:00 2011 +0100
12.3 @@ -92,7 +92,7 @@
12.4 Calc ("HOL.eq",eval_equal "#equal_")
12.5 ];
12.6 val SOME (t',_) = rewrite_set_ thy false testrls t;
12.7 -if term2str t' = "True" then ()
12.8 +if term2str t' = "HOL.True" then ()
12.9 else error "eqsystem.sml: length_ [x+y=1,y=2] = 2";
12.10
12.11 val SOME t = parse EqSystem.thy "solution L";
13.1 --- a/test/Tools/isac/Knowledge/poly.sml Thu Mar 10 15:19:26 2011 +0100
13.2 +++ b/test/Tools/isac/Knowledge/poly.sml Thu Mar 10 16:04:00 2011 +0100
13.3 @@ -187,7 +187,7 @@
13.4 SOME (_, Const ("HOL.Trueprop", _) $
13.5 (Const ("HOL.eq", _) $
13.6 (Const ("Poly.is'_multUnordered", _) $ _) $
13.7 - Const ("True", _))) => ()
13.8 + Const ("HOL.True", _))) => ()
13.9 | _ => error "poly.sml diff. eval_is_multUnordered";
13.10
13.11 "----- rewrite_set_ STILL DIDN'T WORK";
14.1 --- a/test/Tools/isac/Knowledge/polyeq.sml Thu Mar 10 15:19:26 2011 +0100
14.2 +++ b/test/Tools/isac/Knowledge/polyeq.sml Thu Mar 10 16:04:00 2011 +0100
14.3 @@ -46,54 +46,54 @@
14.4
14.5 val t2 = (term_of o the o (parse thy)) "(-8 - 2*x + x^^^2) is_expanded_in x";
14.6 val SOME (t,_) = rewrite_set_ PolyEq.thy false PolyEq_prls t2;
14.7 - if (term2str t) = "True" then ()
14.8 + if (term2str t) = "HOL.True" then ()
14.9 else error "polyeq.sml: diff.behav. 1 in is_expended_in";
14.10
14.11 val t0 = (term_of o the o (parse thy)) "(sqrt(x)) is_poly_in x";
14.12 val SOME (t,_) = rewrite_set_ PolyEq.thy false PolyEq_prls t0;
14.13 - if (term2str t) = "False" then ()
14.14 + if (term2str t) = "HOL.False" then ()
14.15 else error "polyeq.sml: diff.behav. 2 in is_poly_in";
14.16
14.17
14.18 val t3 = (term_of o the o (parse thy)) "(-8 + (-1)*2*x + x^^^2) is_poly_in x";
14.19 val SOME (t,_) = rewrite_set_ PolyEq.thy false PolyEq_prls t3;
14.20 - if (term2str t) = "True" then ()
14.21 + if (term2str t) = "HOL.True" then ()
14.22 else error "polyeq.sml: diff.behav. 3 in is_poly_in";
14.23
14.24
14.25 val t4 = (term_of o the o (parse thy)) "(lhs (-8 + (-1)*2*x + x^^^2 = 0)) is_expanded_in x";
14.26 val SOME (t,_) = rewrite_set_ PolyEq.thy false PolyEq_prls t4;
14.27 - if (term2str t) = "True" then ()
14.28 + if (term2str t) = "HOL.True" then ()
14.29 else error "polyeq.sml: diff.behav. 4 in is_expended_in";
14.30
14.31
14.32 val t6 = (term_of o the o (parse thy)) "(lhs (-8 - 2*x + x^^^2 = 0)) is_expanded_in x";
14.33 val SOME (t,_) = rewrite_set_ PolyEq.thy false PolyEq_prls t6;
14.34 - if (term2str t) = "True" then ()
14.35 + if (term2str t) = "HOL.True" then ()
14.36 else error "polyeq.sml: diff.behav. 5 in is_expended_in";
14.37
14.38 val t3 = (term_of o the o (parse thy))"((-8 - 2*x + x^^^2) has_degree_in x) = 2";
14.39 val SOME (t,_) = rewrite_set_ PolyEq.thy false PolyEq_prls t3;
14.40 - if (term2str t) = "True" then ()
14.41 + if (term2str t) = "HOL.True" then ()
14.42 else error "polyeq.sml: diff.behav. in has_degree_in_in";
14.43
14.44
14.45 val t3 = (term_of o the o (parse thy)) "((sqrt(x)) has_degree_in x) = 2";
14.46 val SOME (t,_) = rewrite_set_ PolyEq.thy false PolyEq_prls t3;
14.47 - if (term2str t) = "False" then ()
14.48 + if (term2str t) = "HOL.False" then ()
14.49 else error "polyeq.sml: diff.behav. 6 in has_degree_in_in";
14.50
14.51 val t4 = (term_of o the o (parse thy))
14.52 "((-8 - 2*x + x^^^2) has_degree_in x) = 1";
14.53 val SOME (t,_) = rewrite_set_ PolyEq.thy false PolyEq_prls t4;
14.54 - if (term2str t) = "False" then ()
14.55 + if (term2str t) = "HOL.False" then ()
14.56 else error "polyeq.sml: diff.behav. 7 in has_degree_in_in";
14.57
14.58
14.59 val t5 = (term_of o the o (parse thy))
14.60 "((-8 - 2*x + x^^^2) has_degree_in x) = 2";
14.61 val SOME (t,_) = rewrite_set_ PolyEq.thy false PolyEq_prls t5;
14.62 - if (term2str t) = "True" then ()
14.63 + if (term2str t) = "HOL.True" then ()
14.64 else error "polyeq.sml: diff.behav. 8 in has_degree_in_in";
14.65
14.66
14.67 @@ -848,7 +848,7 @@
14.68 val t1 = (term_of o the o (parse thy)) "0 <= (10/3/2)^^^2 - 1";
14.69 val SOME (t,_) = rewrite_set_ PolyEq.thy false PolyEq_erls t1;
14.70 val t' = term2str t;
14.71 - (*if t'= "True" then ()
14.72 + (*if t'= "HOL.True" then ()
14.73 else error "polyeq.sml: diff.behav. in 'rewrite_set_.. PolyEq_erls";*)
14.74 (* *)
14.75 val fmz = ["equality (3 - 10*x + 3*x^^^2 = 0)",
15.1 --- a/test/Tools/isac/Knowledge/polyminus.sml Thu Mar 10 15:19:26 2011 +0100
15.2 +++ b/test/Tools/isac/Knowledge/polyminus.sml Thu Mar 10 16:04:00 2011 +0100
15.3 @@ -616,7 +616,7 @@
15.4 trace_rewrite := true;
15.5 val SOME (t', _) = rewrite_set_ thy false prls t;
15.6 trace_rewrite := false;
15.7 -if term2str t' = "False" then ()
15.8 +if term2str t' = "HOL.False" then ()
15.9 else error "polyminus.sml Not (matchsub (?a * (?b + ?c)) (8 ...";
15.10 ============ inhibit exn =====================================================*)
15.11
16.1 --- a/test/Tools/isac/Knowledge/rateq.sml Thu Mar 10 15:19:26 2011 +0100
16.2 +++ b/test/Tools/isac/Knowledge/rateq.sml Thu Mar 10 16:04:00 2011 +0100
16.3 @@ -14,22 +14,22 @@
16.4 val t = (term_of o the o (parse RatEq.thy)) "(1/b+1/x=1) is_ratequation_in x";
16.5 val SOME(t_, _) = rewrite_set_ RatEq.thy false RatEq_prls t;
16.6 val result = term2str t_;
16.7 -if result <> "True" then error "rateq.sml: new behaviour 1:" else ();
16.8 +if result <> "HOL.True" then error "rateq.sml: new behaviour 1:" else ();
16.9
16.10 val t = (term_of o the o (parse RatEq.thy)) "(sqrt(x)=1) is_ratequation_in x";
16.11 val SOME(t_, _) = rewrite_set_ RatEq.thy false RatEq_prls t;
16.12 val result = term2str t_;
16.13 -if result <> "False" then error "rateq.sml: new behaviour 2:" else ();
16.14 +if result <> "HOL.False" then error "rateq.sml: new behaviour 2:" else ();
16.15
16.16 val t = (term_of o the o (parse RatEq.thy)) "(x=-1) is_ratequation_in x";
16.17 val SOME(t_,_) = rewrite_set_ RatEq.thy false RatEq_prls t;
16.18 val result = term2str t_;
16.19 -if result <> "False" then error "rateq.sml: new behaviour 3:" else ();
16.20 +if result <> "HOL.False" then error "rateq.sml: new behaviour 3:" else ();
16.21
16.22 val t = (term_of o the o (parse RatEq.thy)) "(3 + x^^^2 + 1/(x^^^2+3)=1) is_ratequation_in x";
16.23 val SOME(t_,_) = rewrite_set_ RatEq.thy false RatEq_prls t;
16.24 val result = term2str t_;
16.25 -if result <> "True" then error "rateq.sml: new behaviour 4:" else ();
16.26 +if result <> "HOL.True" then error "rateq.sml: new behaviour 4:" else ();
16.27
16.28 val result = match_pbl ["equality (x=1)","solveFor x","solutions L"]
16.29 (get_pbt ["rational","univariate","equation"]);
17.1 --- a/test/Tools/isac/Knowledge/rational.sml Thu Mar 10 15:19:26 2011 +0100
17.2 +++ b/test/Tools/isac/Knowledge/rational.sml Thu Mar 10 16:04:00 2011 +0100
17.3 @@ -1005,10 +1005,10 @@
17.4 (*trace_rewrite:=true;*)
17.5 val t = str2term "Not (6*x is_atom)";
17.6 val SOME (t',_) = rewrite_set_ thy false powers_erls t; term2str t';
17.7 -"True";
17.8 +"HOL.True";
17.9 val t = str2term "1 < 2";
17.10 val SOME (t',_) = rewrite_set_ thy false powers_erls t; term2str t';
17.11 -"True";
17.12 +"HOL.True";
17.13
17.14 val t = str2term "(6*x)^^^2";
17.15 val SOME (t',_) = rewrite_ thy dummy_ord powers_erls false
18.1 --- a/test/Tools/isac/Knowledge/rlang.sml Thu Mar 10 15:19:26 2011 +0100
18.2 +++ b/test/Tools/isac/Knowledge/rlang.sml Thu Mar 10 16:04:00 2011 +0100
18.3 @@ -1354,7 +1354,7 @@
18.4 (*EO WN060310 something wrong:
18.5 ([6, 6, 3, 1], Frm) "-1064944 + 32 * x + -48 * x ^^^ 2 = 0"
18.6 ### or2list False
18.7 -([6, 6, 3, 1], Res) "False"
18.8 +([6, 6, 3, 1], Res) "HOL.False"
18.9 *)
18.10 val fmz = ["equality (2*sqrt(261 - x) - sqrt(2+2*x)=sqrt(2)*sqrt(5 - 3*x))",
18.11 "solveFor x","solutions L"];
19.1 --- a/test/Tools/isac/Knowledge/rooteq.sml Thu Mar 10 15:19:26 2011 +0100
19.2 +++ b/test/Tools/isac/Knowledge/rooteq.sml Thu Mar 10 16:04:00 2011 +0100
19.3 @@ -18,62 +18,62 @@
19.4 val t = (term_of o the o (parse RootEq.thy)) "(sqrt(2+x+3)) is_rootTerm_in x";
19.5 val SOME(t_, _) = rewrite_set_ RootEq.thy false RootEq_prls t;
19.6 val result = term2str t_;
19.7 -if result <> "True" then error "rooteq.sml: new behaviour:" else ();
19.8 +if result <> "HOL.True" then error "rooteq.sml: new behaviour:" else ();
19.9
19.10 val t = (term_of o the o (parse RootEq.thy)) "(sqrt(2+x+3)) is_rootTerm_in x";
19.11 val SOME(t_, _) = rewrite_set_ RootEq.thy false RootEq_prls t;
19.12 val result = term2str t_;
19.13 -if result <> "True" then error "rooteq.sml: new behaviour:" else ();
19.14 +if result <> "HOL.True" then error "rooteq.sml: new behaviour:" else ();
19.15
19.16 val t = (term_of o the o (parse RootEq.thy)) "(nroot 5 (x+4)) is_rootTerm_in x";
19.17 val SOME(t_, _) = rewrite_set_ RootEq.thy false RootEq_prls t;
19.18 val result = term2str t_;
19.19 -if result <> "True" then error "rooteq.sml: new behaviour:" else ();
19.20 +if result <> "HOL.True" then error "rooteq.sml: new behaviour:" else ();
19.21
19.22 val t = (term_of o the o (parse RootEq.thy)) "(sqrt(2+x+3)) is_sqrtTerm_in x";
19.23 val SOME(t_, _) = rewrite_set_ RootEq.thy false RootEq_prls t;
19.24 val result = term2str t_;
19.25 -if result <> "True" then error "rooteq.sml: new behaviour:" else ();
19.26 +if result <> "HOL.True" then error "rooteq.sml: new behaviour:" else ();
19.27
19.28 val t = (term_of o the o (parse RootEq.thy)) "(sqrt(25)) is_sqrtTerm_in x";
19.29 val SOME(t_, _) = rewrite_set_ RootEq.thy false RootEq_prls t;
19.30 val result = term2str t_;
19.31 -if result <> "False" then error "rooteq.sml: new behaviour:" else ();
19.32 +if result <> "HOL.False" then error "rooteq.sml: new behaviour:" else ();
19.33
19.34 val t = (term_of o the o (parse RootEq.thy)) "sqrt(1 + x) is_normSqrtTerm_in x";
19.35 val SOME(t_, _) = rewrite_set_ RootEq.thy false RootEq_prls t;
19.36 val result = term2str t_;
19.37 -if result <> "True" then error "rooteq.sml: new behaviour:" else ();
19.38 +if result <> "HOL.True" then error "rooteq.sml: new behaviour:" else ();
19.39
19.40 val t = (term_of o the o (parse RootEq.thy)) "(3+3*sqrt(x)) is_normSqrtTerm_in x";
19.41 val SOME(t_, _) = rewrite_set_ RootEq.thy false RootEq_prls t;
19.42 val result = term2str t_;
19.43 -if result <> "True" then error "rooteq.sml: new behaviour:" else ();
19.44 +if result <> "HOL.True" then error "rooteq.sml: new behaviour:" else ();
19.45
19.46 val t = (term_of o the o (parse RootEq.thy)) "(sqrt(x+1)+1) is_normSqrtTerm_in x";
19.47 val SOME(t_, _) = rewrite_set_ RootEq.thy false RootEq_prls t;
19.48 val result = term2str t_;
19.49 -if result <> "False" then error "rooteq.sml: new behaviour:" else ();
19.50 +if result <> "HOL.False" then error "rooteq.sml: new behaviour:" else ();
19.51
19.52 val t = (term_of o the o (parse RootEq.thy)) "(1 - u/(sqrt(r - u))) is_normSqrtTerm_in u";
19.53 val SOME(t_, _) = rewrite_set_ RootEq.thy false RootEq_prls t;
19.54 val result = term2str t_;
19.55 -if result <> "False" then error "rooteq.sml: new behaviour:" else ();
19.56 +if result <> "HOL.False" then error "rooteq.sml: new behaviour:" else ();
19.57
19.58 val t = (term_of o the o (parse RootEq.thy)) "(x*(1+x)/(sqrt(x+1))) is_normSqrtTerm_in x";
19.59 val SOME(t_, _) = rewrite_set_ RootEq.thy false RootEq_prls t;
19.60 val result = term2str t_;
19.61 -if result <> "True" then error "rooteq.sml: new behaviour:" else ();
19.62 +if result <> "HOL.True" then error "rooteq.sml: new behaviour:" else ();
19.63
19.64 val t = (term_of o the o (parse RootEq.thy)) "(1 - (sqrt(2+x+3)^^^3)) is_normSqrtTerm_in x";
19.65 val SOME(t_, _) = rewrite_set_ RootEq.thy false RootEq_prls t;
19.66 val result = term2str t_;
19.67 -if result <> "False" then error "rooteq.sml: new behaviour:" else ();
19.68 +if result <> "HOL.False" then error "rooteq.sml: new behaviour:" else ();
19.69
19.70 val t = (term_of o the o (parse RootEq.thy)) "(1 + (sqrt(2+x+3)^^^3)) is_normSqrtTerm_in x";
19.71 val SOME(t_, _) = rewrite_set_ RootEq.thy false RootEq_prls t;
19.72 val result = term2str t_;
19.73 -if result <> "True" then error "rooteq.sml: new behaviour:" else ();
19.74 +if result <> "HOL.True" then error "rooteq.sml: new behaviour:" else ();
19.75
19.76
19.77
19.78 @@ -293,7 +293,7 @@
19.79 (*val nxt = Specify_Method ["PolyEq","solve_d0_polyeq_equation"]) *)
19.80 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
19.81 val (p,_,f,nxt,_,pt) = me nxt p c pt;
19.82 -(*val p = ([6,3,1],Res) val f = Form' (FormKF (~1,EdUndef,3,Nundef,"True"))
19.83 +(*val p = ([6,3,1],Res) val f = Form' (FormKF (~1,EdUndef,3,Nundef,"HOL.True"))
19.84 val nxt = ("Or_to_List",Or_to_List) : string * tac*)
19.85 val (p,_,f,nxt,_,pt) = me nxt p c pt;
19.86 (*val p = ([6,3,2],Res) val f = (~1,EdUndef,3,Nundef,"UniversalList"))
20.1 --- a/test/Tools/isac/Knowledge/rootrateq.sml Thu Mar 10 15:19:26 2011 +0100
20.2 +++ b/test/Tools/isac/Knowledge/rootrateq.sml Thu Mar 10 16:04:00 2011 +0100
20.3 @@ -14,37 +14,37 @@
20.4 *)
20.5 val t1 = (term_of o the o (parse thy)) "(-8 - sqrt(x) + x^^^2) is_rootRatAddTerm_in x";
20.6 val SOME (t,_) = rewrite_set_ RootRatEq.thy false RootRatEq_prls t1;
20.7 -if (term2str t) = "False" then ()
20.8 +if (term2str t) = "HOL.False" then ()
20.9 else error "rootrateq.sml: diff.behav. 1 in is_rootRatAddTerm_in";
20.10
20.11 val t1 = (term_of o the o (parse thy)) "(1/x) is_rootRatAddTerm_in x";
20.12 val SOME (t,_) = rewrite_set_ RootRatEq.thy false RootRatEq_prls t1;
20.13 -if (term2str t) = "False" then ()
20.14 +if (term2str t) = "HOL.False" then ()
20.15 else error "rootrateq.sml: diff.behav. 2 in is_rootRatAddTerm_in";
20.16
20.17 val t1 = (term_of o the o (parse thy)) "(1/sqrt(x)) is_rootRatAddTerm_in x";
20.18 val SOME (t,_) = rewrite_set_ RootRatEq.thy false RootRatEq_prls t1;
20.19 -if (term2str t) = "False" then ()
20.20 +if (term2str t) = "HOL.False" then ()
20.21 else error "rootrateq.sml: diff.behav. 3 in is_rootRatAddTerm_in";
20.22
20.23 val t1 = (term_of o the o (parse thy)) "(1/(sqrt(x)+1)) is_rootRatAddTerm_in x";
20.24 val SOME (t,_) = rewrite_set_ RootRatEq.thy false RootRatEq_prls t1;
20.25 -if (term2str t) = "True" then ()
20.26 +if (term2str t) = "HOL.True" then ()
20.27 else error "rootrateq.sml: diff.behav. 4 in is_rootRatAddTerm_in";
20.28
20.29 val t1 = (term_of o the o (parse thy)) "(3 + 1/(1+sqrt(x))) is_rootRatAddTerm_in x";
20.30 val SOME (t,_) = rewrite_set_ RootRatEq.thy false RootRatEq_prls t1;
20.31 -if (term2str t) = "True" then ()
20.32 +if (term2str t) = "HOL.True" then ()
20.33 else error "rootrateq.sml: diff.behav. 5 in is_rootRatAddTerm_in";
20.34
20.35 val t1 = (term_of o the o (parse thy)) "(1/(1+sqrt(y)) + 3 + 1/(1+sqrt(x))) is_rootRatAddTerm_in x";
20.36 val SOME (t,_) = rewrite_set_ RootRatEq.thy false RootRatEq_prls t1;
20.37 -if (term2str t) = "True" then ()
20.38 +if (term2str t) = "HOL.True" then ()
20.39 else error "rootrateq.sml: diff.behav. 6 in is_rootRatAddTerm_in";
20.40
20.41 val t1 = (term_of o the o (parse thy)) "(1/(1+sqrt(x)) + 3 + 1/(1+sqrt(y))) is_rootRatAddTerm_in x";
20.42 val SOME (t,_) = rewrite_set_ RootRatEq.thy false RootRatEq_prls t1;
20.43 -if (term2str t) = "True" then ()
20.44 +if (term2str t) = "HOL.True" then ()
20.45 else error "rootrateq.sml: diff.behav. 7 in is_rootRatAddTerm_in";
20.46
20.47
21.1 --- a/test/Tools/isac/ProgLang/calculate.sml Thu Mar 10 15:19:26 2011 +0100
21.2 +++ b/test/Tools/isac/ProgLang/calculate.sml Thu Mar 10 16:04:00 2011 +0100
21.3 @@ -48,6 +48,9 @@
21.4 val t = (term_of o the o (parse thy)) "((1+2)*4/3)^^^2";
21.5 val SOME (thmID,thm) = get_calculation_ thy (the(assoc(calclist,"PLUS"))) t;
21.6 (*========== inhibit exn =======================================================
21.7 +WN110310: cterm_of: val thm = "^AE1^AA + ^AE2^AA = ^AE3^AA" [.]: thm
21.8 + probably drop Free ("123",...
21.9 +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
21.10 val SOME (t,_) = rewrite_ thy tless_true tval_rls true thm t;
21.11 term2str t = "(3 * 4 / 3) ^^^ 2";
21.12
21.13 @@ -189,7 +192,7 @@
21.14 val t = (term_of o the o (parse Test.thy)) "2 is_const";
21.15 atomty t;
21.16 rewrite_set_ Test.thy false tval_rls t;
21.17 -(*val it = SOME (Const ("True","bool"),[]) ... works*)
21.18 +(*val it = SOME (Const ("HOL.True","bool"),[]) ... works*)
21.19
21.20 val t = str2term "2 * x is_const";
21.21 val SOME (str,t') = eval_const "" "" t (theory "Isac");
21.22 @@ -473,6 +476,6 @@
21.23
21.24 val SOME (t',_) = rewrite_set_ Test.thy false tval_rls t;
21.25 term2str t';
21.26 -"False";
21.27 +"HOL.False";
21.28 ===== inhibit exn ?===========================================================*)
21.29
22.1 --- a/test/Tools/isac/ProgLang/rewrite.sml Thu Mar 10 15:19:26 2011 +0100
22.2 +++ b/test/Tools/isac/ProgLang/rewrite.sml Thu Mar 10 16:04:00 2011 +0100
22.3 @@ -37,7 +37,6 @@
22.4 val bdv = [];
22.5 val r = (((inst_bdv bdv) o norm o #prop o rep_thm) thm);
22.6 "----- from old: and rew_sub";
22.7 -(*========== inhibit exn =======================================================
22.8 val (lhs,rhs) = (dest_equals' o strip_trueprop
22.9 o Logic.strip_imp_concl) r;
22.10 (* old
22.11 @@ -75,7 +74,6 @@
22.12 Pretty.writeln (ProofContext.pretty_term_abbrev @{context} r');
22.13 Pretty.writeln (ProofContext.pretty_term_abbrev @{context} t');
22.14 (*}*)
22.15 -============ inhibit exn =====================================================*)
22.16
22.17 "----------- test rewriting without Isac's thys ---------";
22.18 "----------- test rewriting without Isac's thys ---------";
22.19 @@ -86,7 +84,6 @@
22.20 val ctxt = @{context};
22.21 val thm = @{thm add_commute};
22.22 val tm = @{term "x + y*z::real"};
22.23 -(*-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.
22.24
22.25 val SOME (r,_) = (rewrite_ thy dummy_ord e_rls false thm tm)
22.26 handle _ => error "rewrite.sml diff.behav. in rewriting";
22.27 @@ -114,7 +111,6 @@
22.28 val tm = @{term "x*y + z::real"};
22.29 val SOME (r,_) = (rewrite_ thy tord e_rls false thm tm)
22.30 handle _ => error "rewrite.sml diff.behav. in rewriting";
22.31 --.-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.*)
22.32
22.33
22.34 "----------- conditional rewriting without Isac's thys --";
22.35 @@ -184,7 +180,7 @@
22.36 val p' = map HOLogic.dest_Trueprop ((fst o Logic.strip_prems)
22.37 (Logic.count_prems r', [], r'));
22.38 case p' of
22.39 - [Const ("Not", _) $ (Const ("HOL.eq", _) $ Free ("y", _) $
22.40 + [Const ("HOL.Not", _) $ (Const ("HOL.eq", _) $ Free ("y", _) $
22.41 Const ("Groups.zero_class.zero", _))] => ()
22.42 | _ => error "rewrite.sml assumption changed";
22.43 "=====^^^ make asms without Trueprop ---^^^";
22.44 @@ -198,7 +194,7 @@
22.45 "----------- step through 'fun rewrite_terms_' ---------";
22.46 "----- step 0: args for rewrite_terms_, local fun";
22.47 val (thy, ord, erls, equs, t) =
22.48 - (theory "Biegelinie", dummy_ord, Erls, [str2term "x = 0"],
22.49 + (@{theory "Biegelinie"}, dummy_ord, Erls, [str2term "x = 0"],
22.50 str2term "M_b x = -1 * q_0 * x ^^^ 2 / 2 + x * c + c_2");
22.51 "----- step 1: args for rew_";
22.52 val ((t', asm'), (rules as r::rs), t) = ((e_term, []), equs, t);
22.53 @@ -298,7 +294,7 @@
22.54 ----- 2009 -------------------------------------------------------------------*)
22.55
22.56 (*the situation as was before repair (asm without Trueprop) is outcommented*)
22.57 -val thy = theory "Isac";
22.58 +val thy = @{theory "Isac"};
22.59 "===== example which raised the problem =================";
22.60 val t = @{term "1 / EI * (L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2)"};
22.61 "----- rewrite_set_inst_ norm_Rational_noadd_fractions--";
22.62 @@ -343,7 +339,6 @@
22.63 trace_rewrite := false; (*<<<<<<<<<<<<<<<<<<<<<###############################*)
22.64 "--------------------------------------------------------";
22.65
22.66 -
22.67 "----------- compare all prepat's existing 2010 ---------";
22.68 "----------- compare all prepat's existing 2010 ---------";
22.69 "----------- compare all prepat's existing 2010 ---------";
22.70 @@ -375,7 +370,7 @@
22.71 |> writeln
22.72 *}
22.73 end *)
22.74 -val thy = theory "Isac";
22.75 +val thy = @{theory "Isac"};
22.76 val t = @{term "a + b * x = (0 ::real)"};
22.77 val pat = parse_patt thy "?l = (?r ::real)";
22.78 val precond = parse_patt thy "is_polynomial (?l::real)";(*no infix def*)
22.79 @@ -441,14 +436,18 @@
22.80 "----------- fun app_rev, Rrls, -------------------------";
22.81 "----------- fun app_rev, Rrls, -------------------------";
22.82 val t = str2term "x^^^2 * x";
22.83 +
22.84 if is_multUnordered t then () else error "rewrite.sml diff. is_multUnordered 2";
22.85 val tm = str2term "(x^^^2 * x) is_multUnordered";
22.86 +eval_is_multUnordered "testid" "" tm thy;
22.87 +
22.88 +(*-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.
22.89 case eval_is_multUnordered "testid" "" tm thy of
22.90 SOME (_, Const ("HOL.Trueprop", _) $
22.91 (Const ("HOL.eq", _) $
22.92 (Const ("Poly.is'_multUnordered", _) $ _) $
22.93 - Const ("True", _))) => ()
22.94 - | _ => error "rewrite.sml diff. eval_is_multUnordered 2";
22.95 + Const ("HOL.True", _))) => ()
22.96 + | _ => error "rewrite.sml diff. eval_is_multUnordered 2b";
22.97
22.98 tracing "----- begin rewrite x^^^2 * x ---"; trace_rewrite := true;
22.99 val SOME (t', _) = rewrite_set_ thy true order_mult_ t;