1.1 --- a/TODO.md Fri Aug 05 11:41:06 2022 +0200
1.2 +++ b/TODO.md Fri Aug 05 12:30:16 2022 +0200
1.3 @@ -8,6 +8,9 @@
1.4 76a77
1.5 > "src/Tools/isac/etc" -> Path.explode("isabelle.isac"),
1.6
1.7 +* MW: Skip_Proof.make_thm: theory -> term -> thm ? could now change signature to
1.8 + : Proof.context -> term -> thm
1.9 +
1.10
1.11 ***** some items for discussion
1.12
1.13 @@ -68,7 +71,6 @@
1.14 ***** priority of WN items is top down, most urgent/simple on top
1.15
1.16 * WN: rewriting with ctxt not complete (cause errors hard to indentify later)
1.17 - - Prconditions.eval
1.18 - Solve_Step.check ..Rewrite_Inst, Substitute, ..
1.19 - Error_Pattern.check_for', fill_form
1.20 - Derive.steps
2.1 --- a/src/Tools/isac/Interpret/derive.sml Fri Aug 05 11:41:06 2022 +0200
2.2 +++ b/src/Tools/isac/Interpret/derive.sml Fri Aug 05 12:30:16 2022 +0200
2.3 @@ -84,7 +84,7 @@
2.4 (msg_3 ctxt t'; rew_once (lim - 1) (rts @ [(t, r, (t', a'))]) t' Appl rrs'))
2.5 | Rule.Eval (c as (op_, _)) =>
2.6 (msg_4 ctxt op_;
2.7 - case Eval.adhoc_thm (Proof_Context.theory_of ctxt) c t of
2.8 + case Eval.adhoc_thm ctxt c t of
2.9 NONE => rew_once lim rts t apno rs'
2.10 | SOME (thmid, tm) =>
2.11 (let
3.1 --- a/src/Tools/isac/MathEngBasic/rewrite.sml Fri Aug 05 11:41:06 2022 +0200
3.2 +++ b/src/Tools/isac/MathEngBasic/rewrite.sml Fri Aug 05 12:30:16 2022 +0200
3.3 @@ -173,7 +173,7 @@
3.4 (* once again try the same rule, e.g. associativity against "()"*)
3.5 | Rule.Eval (cc as (op_, _)) =>
3.6 let val _ = trace_in1 ctxt i "try calc" op_;
3.7 - in case Eval.adhoc_thm (Proof_Context.theory_of ctxt) cc ct of
3.8 + in case Eval.adhoc_thm ctxt cc ct of
3.9 NONE => rew_once ruls asm ct apno thms
3.10 | SOME (_, thm') =>
3.11 let
3.12 @@ -185,7 +185,7 @@
3.13 end
3.14 | Rule.Cal1 (cc as (op_, _)) =>
3.15 let val _ = trace_in1 ctxt i "try cal1" op_;
3.16 - in case Eval.adhoc_thm1_ (Proof_Context.theory_of ctxt) cc ct of
3.17 + in case Eval.adhoc_thm1_ ctxt cc ct of
3.18 NONE => (ct, asm)
3.19 | SOME (_, thm') =>
3.20 let
3.21 @@ -205,7 +205,6 @@
3.22 val _ = trace_eq1 ctxt i "rls" rls ct
3.23 val (ct', asm') = rew_once ruls [] ct Noap ruls;
3.24 in if ct = ct' then NONE else SOME (ct', distinct op = asm') end
3.25 -(*--vvv and app_sub are type correct-----------------------------------------------------------*)
3.26 and app_rev ctxt i rrls t = (* apply an Rrls; if not applicable proceed with subterms*)
3.27 let (* check a (precond, pattern) of a rev-set; stops with 1st true *)
3.28 fun chk_prepat _ _ [] _ = true
3.29 @@ -284,7 +283,7 @@
3.30
3.31 (* search ct for adjacent numerals and calculate them by operator isa_fn *)
3.32 fun calculate_ ctxt (isa_fn as (id, eval_fn)) t =
3.33 - case Eval.adhoc_thm (Proof_Context.theory_of ctxt) isa_fn t of
3.34 + case Eval.adhoc_thm ctxt isa_fn t of
3.35 NONE => NONE
3.36 | SOME (thmID, thm) =>
3.37 (let val rew = case rewrite_ ctxt Rewrite_Ord.function_empty Rule_Set.empty false thm t of
4.1 --- a/src/Tools/isac/MathEngBasic/tactic.sml Fri Aug 05 11:41:06 2022 +0200
4.2 +++ b/src/Tools/isac/MathEngBasic/tactic.sml Fri Aug 05 12:30:16 2022 +0200
4.3 @@ -249,11 +249,11 @@
4.4 SOME _ => [rule2tac ctxt [] thm']
4.5 | NONE => [])
4.6 | try_rew ctxt _ _ _ f (cal as Rule.Eval c) =
4.7 - (case Eval.adhoc_thm (Proof_Context.theory_of ctxt) c f of
4.8 + (case Eval.adhoc_thm ctxt c f of
4.9 SOME _ => [rule2tac ctxt [] cal]
4.10 | NONE => [])
4.11 | try_rew ctxt _ _ _ f (cal as Rule.Cal1 c) =
4.12 - (case Eval.adhoc_thm (Proof_Context.theory_of ctxt) c f of
4.13 + (case Eval.adhoc_thm ctxt c f of
4.14 SOME _ => [rule2tac ctxt [] cal]
4.15 | NONE => [])
4.16 | try_rew thy _ _ subst f (Rule.Rls_ rls) = filter_appl_rews thy subst f rls
5.1 --- a/src/Tools/isac/ProgLang/evaluate.sml Fri Aug 05 11:41:06 2022 +0200
5.2 +++ b/src/Tools/isac/ProgLang/evaluate.sml Fri Aug 05 12:30:16 2022 +0200
5.3 @@ -15,8 +15,8 @@
5.4 val gcd: int -> int -> int
5.5 val sqrt: int -> int
5.6 val cancel_int: int * int -> int * (int * int)
5.7 - val adhoc_thm: theory -> string * Eval_Def.eval_fn -> term -> (string * thm) option
5.8 - val adhoc_thm1_: theory -> Eval_Def.cal -> term -> (string * thm) option
5.9 + val adhoc_thm: Proof.context -> string * Eval_Def.eval_fn -> term -> (string * thm) option
5.10 + val adhoc_thm1_: Proof.context -> Eval_Def.cal -> term -> (string * thm) option
5.11 val norm: term -> term
5.12 val popt2str: ('a * term) option -> string
5.13 val int_of_numeral: term -> int
5.14 @@ -156,17 +156,17 @@
5.15 | get_pair (*7*)_ _ _ _ = NONE
5.16
5.17 (* get a thm from an op_ somewhere in a term by use of get_pair *)
5.18 -fun adhoc_thm thy (op_, eval_fn) t =
5.19 +fun adhoc_thm ctxt (op_, eval_fn) t =
5.20 ((*@{print\<open>tracing\<close>}{a = "adhoc_thm", op_ = op_, t = t, get_p = get_pair thy op_ eval_fn t};*)
5.21 - case get_pair (Proof_Context.init_global thy) op_ eval_fn t of
5.22 + case get_pair ctxt op_ eval_fn t of
5.23 NONE => NONE
5.24 - | SOME (thmid, t') => SOME (thmid, Skip_Proof.make_thm thy t'));
5.25 + | SOME (thmid, t') => SOME (thmid, Skip_Proof.make_thm (Proof_Context.theory_of ctxt) t'));
5.26
5.27 (* get a thm applying an op_ to a term by direct use of eval_fn *)
5.28 -fun adhoc_thm1_ thy (op_, eval_fn) ct =
5.29 - case eval_fn op_ ct (Proof_Context.init_global thy) of
5.30 +fun adhoc_thm1_ ctxt (op_, eval_fn) ct =
5.31 + case eval_fn op_ ct ctxt of
5.32 NONE => NONE
5.33 - | SOME (thmid, t') => SOME (thmid, Skip_Proof.make_thm thy t');
5.34 + | SOME (thmid, t') => SOME (thmid, Skip_Proof.make_thm (Proof_Context.theory_of ctxt) t');
5.35
5.36 (** for ordered and conditional rewriting **)
5.37
6.1 --- a/test/Tools/isac/Knowledge/diophanteq.sml Fri Aug 05 11:41:06 2022 +0200
6.2 +++ b/test/Tools/isac/Knowledge/diophanteq.sml Fri Aug 05 12:30:16 2022 +0200
6.3 @@ -36,10 +36,10 @@
6.4 val SOME (t,_) = rewrite_inst_ ctxt Rewrite_Ord.function_empty Rule_Set.empty true subst
6.5 @{thm "int_isolate_add"} t; UnparseC.term t;
6.6
6.7 -val SOME (thmID,thm) = adhoc_thm thy (the(LibraryC.assoc(KEStore_Elems.get_calcs @{theory},"TIMES"))) t;
6.8 +val SOME (thmID,thm) = adhoc_thm ctxt (the(LibraryC.assoc(KEStore_Elems.get_calcs @{theory},"TIMES"))) t;
6.9 val SOME (t,_) = rewrite_ ctxt tless_true tval_rls true thm t; UnparseC.term t;
6.10
6.11 -val SOME (thmID,thm) = adhoc_thm thy (the(LibraryC.assoc(KEStore_Elems.get_calcs @{theory},"PLUS"))) t;
6.12 +val SOME (thmID,thm) = adhoc_thm ctxt (the(LibraryC.assoc(KEStore_Elems.get_calcs @{theory},"PLUS"))) t;
6.13 val SOME (t,_) = rewrite_ ctxt tless_true tval_rls true thm t; UnparseC.term t;
6.14
6.15 "----------- mathengine with usecase1 -------------------";
6.16 @@ -71,10 +71,10 @@
6.17 SOME t' => t'
6.18 | NONE => error "diophanteq.sml: syntax error in rewriting for usecase2";
6.19
6.20 -val SOME (thmID,thm) = adhoc_thm thy (the(LibraryC.assoc(KEStore_Elems.get_calcs @{theory},"TIMES"))) t;
6.21 +val SOME (thmID,thm) = adhoc_thm ctxt (the(LibraryC.assoc(KEStore_Elems.get_calcs @{theory},"TIMES"))) t;
6.22 val SOME (t,_) = rewrite_ ctxt tless_true tval_rls true thm t; UnparseC.term t;
6.23
6.24 -val SOME (thmID,thm) = adhoc_thm thy (the(LibraryC.assoc(KEStore_Elems.get_calcs @{theory},"PLUS"))) t;
6.25 +val SOME (thmID,thm) = adhoc_thm ctxt (the(LibraryC.assoc(KEStore_Elems.get_calcs @{theory},"PLUS"))) t;
6.26 val SOME (t,_) = rewrite_ ctxt tless_true tval_rls true thm t; UnparseC.term t;
6.27
6.28
7.1 --- a/test/Tools/isac/Knowledge/integrate.sml Fri Aug 05 11:41:06 2022 +0200
7.2 +++ b/test/Tools/isac/Knowledge/integrate.sml Fri Aug 05 12:30:16 2022 +0200
7.3 @@ -102,7 +102,7 @@
7.4 else error "intergrate.sml: diff. eval_add_new_c";
7.5
7.6 val cc = ("Integrate.add_new_c", eval_add_new_c "add_new_c_");
7.7 -val SOME (thmstr, thm) = adhoc_thm1_ thy cc term;
7.8 +val SOME (thmstr, thm) = adhoc_thm1_ @{context} cc term;
7.9
7.10 val SOME (t',_) = rewrite_set_ ctxt true add_new_c term;
7.11 if UnparseC.term t' = "x \<up> 2 * c + c_2 + c_3" then ()
8.1 --- a/test/Tools/isac/MathEngBasic/rewrite.sml Fri Aug 05 11:41:06 2022 +0200
8.2 +++ b/test/Tools/isac/MathEngBasic/rewrite.sml Fri Aug 05 12:30:16 2022 +0200
8.3 @@ -519,7 +519,7 @@
8.4 | Rule.Eval (cc as (op_, _)) =>
8.5 let val _= trace1 i (" try calc: " ^ op_ ^ "'")
8.6 val ct = TermC.uminus_to_string ct (*WN190312: superfluous?*)
8.7 - in case Eval.adhoc_thm thy cc ct of
8.8 + in case Eval.adhoc_thm ctxt cc ct of
8.9 NONE => rew_once ruls asm ct apno thms
8.10 | SOME (_, thm') =>
8.11 let
8.12 @@ -533,7 +533,7 @@
8.13 | Rule.Cal1 (cc as (op_, _)) =>
8.14 let val _= trace1 i (" try cal1: " ^ op_ ^ "'");
8.15 val ct = TermC.uminus_to_string ct
8.16 - in case Eval.adhoc_thm1_ thy cc ct of
8.17 + in case Eval.adhoc_thm1_ @{context} cc ct of
8.18 NONE => (ct, asm)
8.19 | SOME (_, thm') =>
8.20 let
9.1 --- a/test/Tools/isac/ProgLang/evaluate.sml Fri Aug 05 11:41:06 2022 +0200
9.2 +++ b/test/Tools/isac/ProgLang/evaluate.sml Fri Aug 05 12:30:16 2022 +0200
9.3 @@ -37,7 +37,7 @@
9.4 val thy = @{theory "Poly"};
9.5 val cal = snd (assoc_calc' thy "is_polyexp");
9.6 val t = @{term "(x / x) is_polyexp"};
9.7 -val SOME (thmID, thm) = adhoc_thm thy cal t;
9.8 +val SOME (thmID, thm) = adhoc_thm ctxt cal t;
9.9 (HOLogic.dest_Trueprop (Thm.prop_of thm); writeln "all thms wrapped by Trueprop")
9.10 handle TERM _ =>
9.11 error "evaluate.sml: adhoc_thm must return Trueprop";
9.12 @@ -55,22 +55,22 @@
9.13 val pow = (\<^const_name>\<open>realpow\<close>, Calc_Binop.numeric "#power_") : string * Eval_Def.eval_fn;
9.14
9.15 "~~~~~ fun calculate_ , args:"; val (thy, isa_fn, t) = (thy, plus, t);
9.16 -val SOME ("#: 1 + 2 = 3", adh_thm) = adhoc_thm @{theory} isa_fn t;
9.17 +val SOME ("#: 1 + 2 = 3", adh_thm) = adhoc_thm @{context} isa_fn t;
9.18 val SOME (t', []) = rewrite__ ctxt 0 [] Rewrite_Ord.function_empty Rule_Set.empty true adh_thm t;
9.19 if UnparseC.term t' = "(3 * 4 / 3) \<up> 2" then () else error "calculate_ 1 + 2 = 3 changed";
9.20
9.21 "~~~~~ fun calculate_, args:"; val (thy, isa_fn, t) = (thy, times, t');
9.22 -val SOME ("#: 3 * 4 = 12", adh_thm) = adhoc_thm @{theory} isa_fn t';
9.23 +val SOME ("#: 3 * 4 = 12", adh_thm) = adhoc_thm @{context} isa_fn t';
9.24 val SOME (t'', []) = rewrite__ ctxt 0 [] Rewrite_Ord.function_empty Rule_Set.empty true adh_thm t;
9.25 if UnparseC.term t'' = "(12 / 3) \<up> 2" then () else error "calculate_ 3 * 4 = 12 changed";
9.26
9.27 "~~~~~ fun calculate_, args:"; val (thy, isa_fn, t) = (thy, divide, t'');
9.28 -val SOME ("#divide_e12_3", adh_thm) = adhoc_thm @{theory} isa_fn t;
9.29 +val SOME ("#divide_e12_3", adh_thm) = adhoc_thm @{context} isa_fn t;
9.30 val SOME (t''', []) = rewrite__ ctxt 0 [] Rewrite_Ord.function_empty Rule_Set.empty true adh_thm t;
9.31 if UnparseC.term t''' = "4 \<up> 2" then () else error "calculate_ 12 / 3 = 4 changed";
9.32
9.33 "~~~~~ fun calculate_, args:"; val (thy, isa_fn, t) = (thy, pow, t''');
9.34 -val SOME ("#: 4 \<up> 2 = 16", adh_thm) = adhoc_thm @{theory} isa_fn t;
9.35 +val SOME ("#: 4 \<up> 2 = 16", adh_thm) = adhoc_thm @{context} isa_fn t;
9.36 val SOME (t'''', []) = rewrite__ ctxt 0 [] Rewrite_Ord.function_empty Rule_Set.empty true adh_thm t;
9.37 if UnparseC.term t'''' = "16" then () else error "calculate_ 12 / 3 = 4 changed";
9.38
9.39 @@ -224,32 +224,32 @@
9.40
9.41 val thy = @{theory Test};
9.42 val t = TermC.parseNEW' ctxt "12 / 3";
9.43 -val SOME (thmID,thm) = adhoc_thm thy(the(LibraryC.assoc(KEStore_Elems.get_calcs @{theory},"DIVIDE")))t;
9.44 +val SOME (thmID,thm) = adhoc_thm ctxt(the(LibraryC.assoc(KEStore_Elems.get_calcs @{theory},"DIVIDE")))t;
9.45 val SOME (t,_) = rewrite_ ctxt tless_true tval_rls true thm t;
9.46 "12 / 3 = 4";
9.47 val thy = @{theory Test};
9.48 val t = TermC.parseNEW' ctxt "4 \<up> 2";
9.49 -val SOME (thmID,thm) = adhoc_thm thy(the(LibraryC.assoc(KEStore_Elems.get_calcs @{theory},"POWER"))) t;
9.50 +val SOME (thmID,thm) = adhoc_thm ctxt(the(LibraryC.assoc(KEStore_Elems.get_calcs @{theory},"POWER"))) t;
9.51 val SOME (t,_) = rewrite_ ctxt tless_true tval_rls true thm t;
9.52 "4 ^ 2 = 16";
9.53
9.54 val t = TermC.parseNEW' ctxt "((1 + 2) * 4 / 3) \<up> 2";
9.55 - val SOME (thmID,thm) = adhoc_thm thy (the(LibraryC.assoc(KEStore_Elems.get_calcs @{theory},"PLUS"))) t;
9.56 + val SOME (thmID,thm) = adhoc_thm ctxt (the(LibraryC.assoc(KEStore_Elems.get_calcs @{theory},"PLUS"))) t;
9.57 "1 + 2 = 3";
9.58 val SOME (t,_) = rewrite_ ctxt tless_true tval_rls true thm t;
9.59 UnparseC.term t;
9.60 "(3 * 4 / 3) \<up> 2";
9.61 - val SOME (thmID,thm) = adhoc_thm thy (the(LibraryC.assoc(KEStore_Elems.get_calcs @{theory},"TIMES")))t;
9.62 + val SOME (thmID,thm) = adhoc_thm ctxt (the(LibraryC.assoc(KEStore_Elems.get_calcs @{theory},"TIMES")))t;
9.63 "3 * 4 = 12";
9.64 val SOME (t,_) = rewrite_ ctxt tless_true tval_rls true thm t;
9.65 UnparseC.term t;
9.66 "(12 / 3) \<up> 2";
9.67 - val SOME (thmID,thm) =adhoc_thm thy(the(LibraryC.assoc(KEStore_Elems.get_calcs @{theory},"DIVIDE")))t;
9.68 + val SOME (thmID,thm) =adhoc_thm ctxt(the(LibraryC.assoc(KEStore_Elems.get_calcs @{theory},"DIVIDE")))t;
9.69 "12 / 3 = 4";
9.70 val SOME (t,_) = rewrite_ ctxt tless_true tval_rls true thm t;
9.71 UnparseC.term t;
9.72 "4 \<up> 2";
9.73 - val SOME (thmID,thm) = adhoc_thm thy(the(LibraryC.assoc(KEStore_Elems.get_calcs @{theory},"POWER")))t;
9.74 + val SOME (thmID,thm) = adhoc_thm ctxt(the(LibraryC.assoc(KEStore_Elems.get_calcs @{theory},"POWER")))t;
9.75 "4 \<up> 2 = 16";
9.76 val SOME (t,_) = rewrite_ ctxt tless_true tval_rls true thm t;
9.77 UnparseC.term t;
9.78 @@ -260,7 +260,7 @@
9.79 (*13.9.02 *** calc: operator = pow not defined*)
9.80 val t = TermC.parseNEW' ctxt "3 \<up> 2";
9.81 val SOME (thmID,thm) =
9.82 - adhoc_thm thy (the(LibraryC.assoc(KEStore_Elems.get_calcs @{theory},"POWER"))) t;
9.83 + adhoc_thm ctxt (the(LibraryC.assoc(KEStore_Elems.get_calcs @{theory},"POWER"))) t;
9.84 (*** calc: operator = pow not defined*)
9.85
9.86 val (op_, eval_fn) = the (LibraryC.assoc(KEStore_Elems.get_calcs @{theory},"POWER"));
9.87 @@ -388,7 +388,7 @@
9.88 (*--------------------------------------------------------------------vvvvvvvvvv*)
9.89 val SOME (isa_str, eval_fn) = LibraryC.assoc (KEStore_Elems.get_calcs @{theory}, "is_num");
9.90 val t = @{term "9 is_num"};
9.91 -val SOME (str, thm) = adhoc_thm thy (isa_str, eval_fn) t;
9.92 +val SOME (str, thm) = adhoc_thm ctxt (isa_str, eval_fn) t;
9.93 if str = "#is_num_9_" andalso ThmC_Def.string_of_thm thm = "(9 is_num) = True"
9.94 then () else error "adhoc_thm 9 is_num changed";
9.95
9.96 @@ -398,23 +398,23 @@
9.97 if isa_str = "Orderings.ord_class.less" then () else error "adhoc_thm (4 < 4) = False CHANGED";
9.98
9.99 val t = @{term "4 < (4 :: real)"};
9.100 -val SOME (str, thm) = adhoc_thm thy (isa_str, eval_fn) t;
9.101 +val SOME (str, thm) = adhoc_thm ctxt (isa_str, eval_fn) t;
9.102 if str = "#less_4_4" andalso ThmC_Def.string_of_thm thm = "(4 < 4) = False"
9.103 then () else error "adhoc_thm 4 < 4 changed";
9.104
9.105 val SOME t = parseNEW @{context} "a < 4";
9.106 -case adhoc_thm thy (isa_str, eval_fn) t of
9.107 +case adhoc_thm ctxt (isa_str, eval_fn) t of
9.108 NONE => () | _ => error "adhoc_thm a < 4 does NOT result in NONE";
9.109
9.110 val SOME (isa_str, eval_fn) = LibraryC.assoc (KEStore_Elems.get_calcs @{theory}, "PLUS");
9.111 val SOME t = parseNEW @{context} "1 + (2::real)";
9.112 -val SOME (str, thm) = adhoc_thm thy (isa_str, eval_fn) t;
9.113 +val SOME (str, thm) = adhoc_thm ctxt (isa_str, eval_fn) t;
9.114 if str = "#: 1 + 2 = 3" andalso ThmC_Def.string_of_thm thm = "1 + 2 = 3"
9.115 then () else error "adhoc_thm 1 + 2 changed";
9.116
9.117 val SOME (isa_str, eval_fn) = LibraryC.assoc (KEStore_Elems.get_calcs @{theory}, "DIVIDE");
9.118 val t = @{term "6 / -8 :: real"};
9.119 -val SOME (str, thm) = adhoc_thm thy (isa_str, eval_fn) t;
9.120 +val SOME (str, thm) = adhoc_thm ctxt (isa_str, eval_fn) t;
9.121 if str = "#divide_e6_~8" andalso ThmC_Def.string_of_thm thm = "6 / - 8 = - 3 / 4"
9.122 then () else error "adhoc_thm 6 / -8 = - 3 / 4 changed";
9.123
9.124 @@ -423,12 +423,12 @@
9.125 val SOME (isa_str, eval_fn) = LibraryC.assoc (KEStore_Elems.get_calcs @{theory}, "ident");
9.126
9.127 val t = @{term "3 =!= (3 :: real)"};
9.128 -val SOME (str, thm) = adhoc_thm thy (isa_str, eval_fn) t;
9.129 +val SOME (str, thm) = adhoc_thm ctxt (isa_str, eval_fn) t;
9.130 if str = "#ident_(3)_(3)" andalso ThmC_Def.string_of_thm thm = "(3 =!= 3) = True"
9.131 then () else error "adhoc_thm (3 =!= 3) changed";
9.132
9.133 val t = @{term "\<not> ((4 :: real) + (4 * x + x \<up> 2) =!= 0)"};
9.134 -val SOME (str, thm) = adhoc_thm thy (isa_str, eval_fn) t;
9.135 +val SOME (str, thm) = adhoc_thm ctxt (isa_str, eval_fn) t;
9.136 if str = "#ident_(4 + (4 * x + x \<up> 2))_(0)" andalso ThmC_Def.string_of_thm thm = "(4 + (4 * x + x \<up> 2) =!= 0) = False"
9.137 then () else error "adhoc_thm (\<not> (4 + (4 * x + x ^ 2) =!= 0)) changed";
9.138
9.139 @@ -448,7 +448,7 @@
9.140
9.141 STEP-INTO BEVORE REMOVING THE ERROR:
9.142 val SOME ("#divide_e~1_2", adhoc_thm) =
9.143 - Eval.adhoc_thm @{theory} eval_ t;
9.144 + Eval.adhoc_thm @{context} eval_ t;
9.145 "~~~~~ fun adhoc_thm , args:"; val (thy, (op_, eval_fn), t) = (@{theory}, eval_, t);
9.146 val SOME
9.147 ("#divide_e~1_2", t'') =
9.148 @@ -460,7 +460,7 @@
9.149 (*+*)ThmC.string_of_thm adhoc_thm = "- 1 / 2 = - 1 / 2"
9.150 *)
9.151
9.152 -val NONE = adhoc_thm @{theory} eval_ t;
9.153 +val NONE = adhoc_thm @{context} eval_ t;
9.154 "~~~~~ fun adhoc_thm , args:"; val (thy, (op_, eval_fn), t) = (@{theory}, eval_, t);
9.155 val NONE =
9.156 (*case*) get_pair ctxt op_ eval_fn t (*of*);
9.157 @@ -470,7 +470,7 @@
9.158 "----------- fun adhoc_thm \<longrightarrow> exception TYPE --------------------------------------------------";
9.159 "----------- fun adhoc_thm \<longrightarrow> exception TYPE --------------------------------------------------";
9.160 val t = TermC.str2term "sqrt 4";
9.161 -Eval.adhoc_thm (ThyC.get_theory "Isac_Knowledge") ("NthRoot.sqrt", eval_sqrt "#sqrt_") t;
9.162 +Eval.adhoc_thm @{context} ("NthRoot.sqrt", eval_sqrt "#sqrt_") t;
9.163
9.164 "~~~~~ fun adhoc_thm , args:"; val (thy, (op_, eval_fn), ct) =
9.165 ((ThyC.get_theory "Isac_Knowledge"),
10.1 --- a/test/Tools/isac/Test_Isac.thy Fri Aug 05 11:41:06 2022 +0200
10.2 +++ b/test/Tools/isac/Test_Isac.thy Fri Aug 05 12:30:16 2022 +0200
10.3 @@ -78,8 +78,8 @@
10.4 "$ISABELLE_ISAC_TEST/Tools/isac/Knowledge/integrate" (* setup for integrate.sml*)
10.5 (**)
10.6 (*\---------------------- do Minisubpbl before ADDTESTS/All_Ctxt ------------------------------/*)
10.7 - "$ISABELLE_ISAC/Knowledge/GCD_Poly_OLD" (*not imported by Isac.thy*)
10.8 - "$ISABELLE_ISAC/Knowledge/GCD_Poly_FP" (*not imported by Isac.thy*)
10.9 + "$ISABELLE_ISAC/Knowledge/GCD_Poly_OLD" (*not imported by Isac.thy*) (*Test_Isac_Short*)
10.10 + "$ISABELLE_ISAC/Knowledge/GCD_Poly_FP" (*not imported by Isac.thy*) (*Test_Isac_Short*)
10.11 (*\---------------------- do Minisubpbl before ADDTESTS/All_Ctxt ------------------------------/*)
10.12 (**)
10.13
10.14 @@ -189,6 +189,7 @@
10.15 (*---------------------- do Minisubpbl before ADDTESTS/All_Ctxt --------------------------------
10.16 ---------------------- do Minisubpbl before ADDTESTS/All_Ctxt --------------------------------*)
10.17
10.18 + ML_file "ProgLang/calculate.sml"
10.19 ML_file "ProgLang/evaluate.sml" (* requires setup from calculate.thy *)
10.20 ML_file "ProgLang/listC.sml"
10.21 ML_file "ProgLang/prog_expr.sml"
10.22 @@ -261,12 +262,10 @@
10.23
10.24 ML_file "BridgeLibisabelle/thy-present.sml"
10.25 ML_file "BridgeLibisabelle/mathml.sml" (*part.*)
10.26 + ML_file "BridgeLibisabelle/pbl-met-hierarchy.sml"
10.27 ML_file "BridgeLibisabelle/thy-hierarchy.sml"
10.28 ML_file "BridgeLibisabelle/interface-xml.sml" (*TODO after 2009-2*)
10.29 ML_file "BridgeLibisabelle/interface.sml"
10.30 -(*WITHOUT inhibit exn WN1130621 Isabelle2012-->13 !thehier! THIS ERROR OCCURS:
10.31 - ... SAME ERROR HERE ON ISABELLE2012 AS IN ISAC ON ISABELLE2011*)
10.32 -
10.33 ML_file "BridgeJEdit/parseC.sml"
10.34 ML_file "BridgeJEdit/preliminary.sml"
10.35 ML_file "BridgeJEdit/vscode-example.sml"
10.36 @@ -274,6 +273,8 @@
10.37 ML_file "Knowledge/delete.sml"
10.38 ML_file "Knowledge/descript.sml"
10.39 ML_file "Knowledge/simplify.sml"
10.40 + ML_file "Knowledge/poly-1.sml"
10.41 +ML_file "Knowledge/poly-2.sml" (*Test_Isac_Short*)
10.42 ML_file "Knowledge/gcd_poly_ml.sml"
10.43 ML_file "Knowledge/rational-1.sml"
10.44 ML_file "Knowledge/rational-2.sml" (*Test_Isac_Short*)
11.1 --- a/test/Tools/isac/Test_Isac_Short.thy Fri Aug 05 11:41:06 2022 +0200
11.2 +++ b/test/Tools/isac/Test_Isac_Short.thy Fri Aug 05 12:30:16 2022 +0200
11.3 @@ -50,14 +50,14 @@
11.4 and find out, which ML_file or *.thy causes an error (might be ONLY one).
11.5 Also backup files (#* ) recognised by jEdit cause this trouble *)
11.6 (*/---------------------- do Minisubpbl before ADDTESTS/All_Ctxt ------------------------------\*)
11.7 -(** )"$ISABELLE_ISAC_TEST/Tools/isac/ADDTESTS/accumulate-val/Thy_All"( *TODOO*)
11.8 +(* "$ISABELLE_ISAC_TEST/ADDTESTS/accumulate-val/Thy_All"(*but ok in editor*)*)
11.9 (**)"$ISABELLE_ISAC_TEST/Tools/isac/ADDTESTS/accumulate-val/Lucas_Interpreter"
11.10 (**)"$ISABELLE_ISAC_TEST/Tools/isac/ADDTESTS/Ctxt"
11.11 (**)"$ISABELLE_ISAC_TEST/Tools/isac/ADDTESTS/test-depend/Build_Test"
11.12 (**)"$ISABELLE_ISAC_TEST/Tools/isac/ADDTESTS/All_Ctxt"
11.13 (**)"$ISABELLE_ISAC_TEST/Tools/isac/ADDTESTS/Test_Units"
11.14 (**)"$ISABELLE_ISAC_TEST/Tools/isac/ADDTESTS/course/phst11/T1_Basics"
11.15 -(** )"$ISABELLE_ISAC_TEST/Tools/isac/ADDTESTS/course/phst11/T2_Rewriting"( *TODOO*)
11.16 +(**)"$ISABELLE_ISAC_TEST/Tools/isac/ADDTESTS/course/phst11/T2_Rewriting"
11.17 (**)"$ISABELLE_ISAC_TEST/Tools/isac/ADDTESTS/course/phst11/T3_MathEngine"
11.18 (**)"$ISABELLE_ISAC_TEST/Tools/isac/ADDTESTS/file-depend/BuildC_Test"
11.19 (**)"$ISABELLE_ISAC_TEST/Tools/isac/ADDTESTS/session-get_theory/Foo"
11.20 @@ -228,7 +228,7 @@
11.21 ML_file "MathEngBasic/thmC.sml"
11.22 ML_file "MathEngBasic/rewrite.sml"
11.23 ML_file "MathEngBasic/tactic.sml"
11.24 - ML_file "MathEngBasic/ctree.sml"
11.25 + ML_file "MathEngBasic/ctree.sml" (*if red, get the file into a text buffer -- this might clear*)
11.26 ML_file "MathEngBasic/calculation.sml"
11.27
11.28 ML_file "Specify/formalise.sml"
11.29 @@ -279,10 +279,9 @@
11.30 ML_file "Knowledge/gcd_poly_ml.sml"
11.31 ML_file "Knowledge/rational-1.sml"
11.32 (*ML_file "Knowledge/rational-2.sml" Test_Isac_Short*)
11.33 -ML_file "Knowledge/equation.sml"
11.34 + ML_file "Knowledge/equation.sml"
11.35 ML_file "Knowledge/root.sml"
11.36 ML_file "Knowledge/lineq.sml"
11.37 -
11.38 (*ML_file "Knowledge/rooteq.sml" some complicated equations not recovered from 2002 *)
11.39 (*ML_file "Knowledge/rateq.sml" some complicated equations not recovered----Test_Isac_Short*)
11.40 ML_file "Knowledge/rootrat.sml"