1.1 --- a/src/Tools/isac/ProgLang/rewrite.sml Sun Feb 25 07:13:47 2018 +0100
1.2 +++ b/src/Tools/isac/ProgLang/rewrite.sml Sun Feb 25 10:19:18 2018 +0100
1.3 @@ -17,36 +17,13 @@
1.4 val rewrite_set_: theory -> bool -> rls -> term -> (term * term list) option
1.5 val rewrite_set_inst_: theory -> bool -> (term * term) list -> rls -> term -> (term * term list) option
1.6 val rewrite_terms_: theory -> ((term * term) list -> term * term -> bool) -> rls -> term list -> term -> (term * term list) option
1.7 -
1.8 -(* doubled intermed., remove !*)
1.9 - val rewrite__set_: theory -> int -> bool -> (term * term) list -> rls -> term -> (term * term list) option
1.10 -
1.11 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
1.12 (* NONE *)
1.13 (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
1.14 -(* probably shift up ---------------
1.15 - exception NO_REWRITE
1.16 - exception STOP_REW_SUB
1.17 - val adhoc_thm': theory' -> string * eval_fn -> cterm' -> thm' option
1.18 + val rewrite__set_: theory -> int -> bool -> (term * term) list -> rls -> term -> (term * term list) option
1.19 val app_rev: theory -> int -> rls -> term -> term * term list * bool
1.20 val app_sub: theory -> int -> rls -> term -> term * term list * bool
1.21 - val calculate: theory' -> string * eval_fn -> cterm' -> (string * thm') option
1.22 - val convert: 'a -> string -> string
1.23 - val convert_metaview_to_thmid: theory -> string -> thm
1.24 - val eval_true': theory' -> rls' -> term -> bool
1.25 - val get_rls_scr: rls' -> scr
1.26 val mk_thm: theory -> string -> thm
1.27 - val mk_thm'': theory -> term -> thm
1.28 - val parse': theory' -> cterm' -> cterm' option
1.29 - val rewrite: theory' -> rew_ord' -> rls' -> bool -> thm' -> cterm' -> (string * string) option
1.30 - val rewrite__: theory -> int -> (term * term) list -> ((term * term) list -> term * term -> bool) -> rls -> bool -> thm -> term -> (term * term list) option
1.31 - val rewrite_inst: theory' -> rew_ord' -> rls' -> bool -> 'a -> thm' -> cterm' -> (cterm' * cterm' list) option
1.32 - val rewrite_set: theory' -> bool -> rls' -> cterm' -> (string * string) option
1.33 - val rewrite_set_inst: theory' -> bool -> subs' -> rls' -> cterm' -> (string * string) option
1.34 - val subs'2subst: theory -> subs' -> subst
1.35 - val trace: int -> string -> unit
1.36 - val trace1: int -> string -> unit
1.37 ---------------------------------------*)
1.38 ( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
1.39 end
1.40
2.1 --- a/test/Tools/isac/Knowledge/atools.sml Sun Feb 25 07:13:47 2018 +0100
2.2 +++ b/test/Tools/isac/Knowledge/atools.sml Sun Feb 25 10:19:18 2018 +0100
2.3 @@ -189,8 +189,8 @@
2.4 if term2str t' = "-6 + -5 * x + -15 * x ^^^ 2 + 0" then ()
2.5 else error "termorder.sml diff.behav ord_make_polynomial_in #14";
2.6
2.7 -val SOME (t',_) = rewrite_set_inst "Isac"false [("bdv","x")] "make_polynomial_in" ppp';
2.8 -if t' = "-6 + -5 * x + -15 * x ^^^ 2 + 0" then ()
2.9 +val SOME (t', _) = rewrite_set_inst_ thy false subst make_polynomial_in ppp;
2.10 +if term2str t' = "-6 + -5 * x + -15 * x ^^^ 2 + 0" then ()
2.11 else error "termorder.sml diff.behav ord_make_polynomial_in #15";
2.12
2.13 val ttt' = "(3*x + 5)/18";
3.1 --- a/test/Tools/isac/Knowledge/diff.sml Sun Feb 25 07:13:47 2018 +0100
3.2 +++ b/test/Tools/isac/Knowledge/diff.sml Sun Feb 25 10:19:18 2018 +0100
3.3 @@ -49,103 +49,62 @@
3.4 "----------- for correction of diff_const ---------------";
3.5 "----------- for correction of diff_const ---------------";
3.6 (*re-evaluate this file, otherwise > *** ME_Isa: 'erls' not known*)
3.7 -val thy' = "Diff";
3.8 -val ct = "Not (x =!= a)";
3.9 -rewrite_set thy' false "erls_diff" ct;
3.10 -val ct = "2 is_const";
3.11 -rewrite_set thy' false "erls_diff" ct;
3.12 +val t = (Thm.term_of o the o (parse thy)) "Not (x =!= a)";
3.13 +case rewrite_set_ thy false erls_diff t of
3.14 + SOME (Const ("HOL.True", _), []) => ()
3.15 +| _ => error "rewrite_set_ Not (x =!= a) changed";
3.16
3.17 -val thm = ("diff_const","");
3.18 -val ct = "d_d x x";
3.19 -val NONE =
3.20 - (rewrite_inst thy' "tless_true" "erls_diff" false [("bdv","x")] thm ct);
3.21 -val ct = "d_d x 2";
3.22 -val SOME (ctt,_) =
3.23 - (rewrite_inst thy' "tless_true" "erls_diff" false [("bdv","x")] thm ct);
3.24 -"----- for 'd_d s a' we got 'a is_const' --> False --------vvv-----";
3.25 -trace_rewrite := false;
3.26 -val ct = "d_d s a";
3.27 - (rewrite_inst thy' "tless_true" "erls_diff" false [("bdv","s")] thm ct);
3.28 -(*got: NONE instead SOME*)
3.29 -eval_true (@{theory "Isac"}) [str2term "a is_const"] (assoc_rls"erls_diff");
3.30 -(*got: false instead true; ~~~~~~~~~~~ replaced by 'is_atom'*)
3.31 -val SOME (ctt,_) =
3.32 - (rewrite_inst thy' "tless_true" "erls_diff" false [("bdv","s")] thm ct);
3.33 -if ctt = "0" then () else error "diff.sml: thm 'diff_const' diff.behav.";
3.34 -trace_rewrite := false;
3.35 -"----- for 'd_d s a' we had 'a is_const' --> False --------^^^-----";
3.36 +val t =(Thm.term_of o the o (parse thy)) "2 is_const";
3.37 +case rewrite_set_ thy false erls_diff t of
3.38 + SOME (Const ("HOL.True", _), []) => ()
3.39 +| _ => error "rewrite_set_ 2 is_const changed";
3.40
3.41 -val thm = ("diff_var","");
3.42 -val ct = "d_d x x";
3.43 -val SOME (ctt,_) =
3.44 - (rewrite_inst thy' "tless_true" "erls_diff" false [("bdv","x")] thm ct);
3.45 -val ct = "d_d x a";
3.46 -val NONE =
3.47 - (rewrite_inst thy' "tless_true" "erls_diff" false [("bdv","x")] thm ct);
3.48 -val ct = "d_d x (x+x)";
3.49 -val NONE =
3.50 -(rewrite_inst thy' "tless_true" "erls_diff" false [("bdv","x")] thm ct);
3.51 -
3.52 +val thm = diff_const;
3.53 +val ct = (Thm.term_of o the o (parse thy)) "d_d x x";
3.54 +val NONE = (rewrite_inst_ thy tless_true erls_diff false subst thm ct);
3.55
3.56 "----------- for correction of diff_quot ----------------";
3.57 "----------- for correction of diff_quot ----------------";
3.58 "----------- for correction of diff_quot ----------------";
3.59 -val thy' = "Diff";
3.60 -val ct = "Not (x = 0)";
3.61 -rewrite_set thy' false "erls_diff" ct;
3.62 +val thy = @{theory "Diff"};
3.63 +val ct = (Thm.term_of o the o (parse thy)) "Not (x = 0)";
3.64 +rewrite_set_ thy false erls_diff ct;
3.65
3.66 -val ct = "d_d x ((x+1) / (x - 1))";
3.67 -val thm = ("diff_quot","");
3.68 +val ct = (Thm.term_of o the o (parse thy)) "d_d x ((x+1) / (x - 1))";
3.69 +val thm = @{thm diff_quot};
3.70 val SOME (ctt,_) =
3.71 - (rewrite_inst thy' "tless_true" "erls_diff" true [("bdv","x")] thm ct);
3.72 -
3.73 + (rewrite_inst_ thy tless_true erls_diff true subst thm ct);
3.74
3.75 "----------- differentiate by rewrite -------------------";
3.76 "----------- differentiate by rewrite -------------------";
3.77 "----------- differentiate by rewrite -------------------";
3.78 -val thy' = "Diff";
3.79 -val ct = "d_d x (x ^^^ 2 + 3 * x + 4)";
3.80 +val thy = @{theory "Diff"};
3.81 +val ct = (Thm.term_of o the o (parse thy)) "d_d x (x ^^^ 2 + 3 * x + 4)";
3.82 "--- 1 ---";
3.83 -val thm = ("diff_sum","");
3.84 -val (ct,_) = the (rewrite_inst thy' "tless_true" "erls_diff" true
3.85 - [("bdv","x::real")] thm ct);
3.86 +val thm = @{thm "diff_sum"};
3.87 +val (ct, _) = the (rewrite_inst_ thy tless_true erls_diff true subst thm ct);
3.88 "--- 2 ---";
3.89 -val (ct,_) = the (rewrite_inst thy' "tless_true" "erls_diff" true
3.90 - [("bdv","x::real")] thm ct);
3.91 +val (ct, _) = the (rewrite_inst_ thy tless_true erls_diff true subst thm ct);
3.92 "--- 3 ---";
3.93 -val thm = ("diff_prod_const","");
3.94 -val (ct,_) = the (rewrite_inst thy' "tless_true" "erls_diff" true
3.95 - [("bdv","x::real")] thm ct);
3.96 +val thm = @{thm "diff_prod_const"};
3.97 +val (ct, _) = the (rewrite_inst_ thy tless_true erls_diff true subst thm ct);
3.98 "--- 4 ---";
3.99 -val thm = ("diff_pow","");
3.100 -val (ct,_) = the (rewrite_inst thy' "tless_true" "erls_diff" true
3.101 - [("bdv","x::real")] thm ct);
3.102 +val thm = @{thm "diff_pow"};
3.103 +val (ct, _) = the (rewrite_inst_ thy tless_true erls_diff true subst thm ct);
3.104 "--- 5 ---";
3.105 -val thm = ("diff_const","");
3.106 -val (ct,_) = the (rewrite_inst thy' "tless_true" "erls_diff" true
3.107 - [("bdv","x::real")] thm ct);
3.108 +val thm = @{thm "diff_const"};
3.109 +val (ct, _) = the (rewrite_inst_ thy tless_true erls_diff true subst thm ct);
3.110 "--- 6 ---";
3.111 -val thm = ("diff_var","");
3.112 -val (ct,_) = the (rewrite_inst thy' "tless_true" "erls_diff" true
3.113 - [("bdv","x::real")] thm ct);
3.114 -if ct = "2 * x ^^^ (2 - 1) + 3 * 1 + 0" then ()
3.115 +val thm = @{thm "diff_var"};
3.116 +val (ct, _) = the (rewrite_inst_ thy tless_true erls_diff true subst thm ct);
3.117 +if term2str ct = "2 * x ^^^ (2 - 1) + 3 * 1 + 0" then ()
3.118 else error "diff.sml diff.behav. in rewrite 1";
3.119 "--- 7 ---";
3.120 -val rls = ("Test_simplify");
3.121 -val (ct,_) = the (rewrite_set thy' false rls ct);
3.122 -if ct="3 + 2 * x" then () else error "new behaviour in test-example";
3.123 -
3.124 -val ct = "2 * x ^^^ (2 - 1) + 3 * 1 + 0";
3.125 -val (ct,_) = the (rewrite_set thy' true rls ct);
3.126 -
3.127 -(*---
3.128 -val t = str2term "x ^^^ (2 - 1)";
3.129 -val SOME (t',_) = rewrite_set_ thy false Test_simplify t;
3.130 -term2str t';
3.131 -
3.132 -val t = str2term "-1 * 1";
3.133 -val SOME (thmID,thm) = adhoc_thm thy (the(assoc(calclist,"times"))) t;
3.134 -*)
3.135 +"--- 7 ---";
3.136 +val rls = Test_simplify;
3.137 +val ct = (Thm.term_of o the o (parse thy)) "2 * x ^^^ (2 - 1) + 3 * 1 + 0";
3.138 +val (ct, _) = the (rewrite_set_ thy true rls ct);
3.139 +if term2str ct = "3 + 2 * x" then () else error "rewrite_set_ Test_simplify 2 changed";
3.140
3.141 "----------- differentiate: me (*+ tacs input*) ---------";
3.142 "----------- differentiate: me (*+ tacs input*) ---------";
4.1 --- a/test/Tools/isac/Knowledge/integrate.sml Sun Feb 25 07:13:47 2018 +0100
4.2 +++ b/test/Tools/isac/Knowledge/integrate.sml Sun Feb 25 10:19:18 2018 +0100
4.3 @@ -252,55 +252,61 @@
4.4 "----------- integrate by ruleset -----------------------";
4.5 "----------- integrate by ruleset -----------------------";
4.6 "----------- integrate by ruleset -----------------------";
4.7 -val rls = "integration_rules";
4.8 -val subs' = [("bdv::real","x::real")];
4.9 -fun rewrit_sinst subs rls str =
4.10 - fst (the (rewrite_set_inst "Integrate" true subs rls str));
4.11 +val thy = @{theory "Integrate"};
4.12 +val rls = integration_rules;
4.13 +val subs = [(@{term "bdv::real"}, @{term "x::real"})];
4.14 (*~~~~~~~~~~~~~~~~~~~~~~~~~~~*)
4.15 -val str = rewrit_sinst subs' rls "Integral x D x";
4.16 -val str = rewrit_sinst subs' rls "Integral c * x ^^^ 2 + c_2 D x";
4.17 -if str = "c * (x ^^^ 3 / 3) + c_2 * x"
4.18 -then () else error "integrate.sml: diff.behav. in integration_rules";
4.19
4.20 -val rls = "add_new_c";
4.21 -val str = rewrit_sinst subs' rls "c * (x ^^^ 3 / 3) + c_2 * x";
4.22 -if str = "c * (x ^^^ 3 / 3) + c_2 * x + c_3" then ()
4.23 +val t = (Thm.term_of o the o (parse thy)) "Integral x D x";
4.24 +val SOME (res, _) = rewrite_set_inst_ thy true subs rls t;
4.25 +if term2str res = "x ^^^ 2 / 2" then () else error "Integral x D x changed";
4.26 +
4.27 +val t = (Thm.term_of o the o (parse thy)) "Integral c * x ^^^ 2 + c_2 D x";
4.28 +val SOME (res, _) = rewrite_set_inst_ thy true subs rls t;
4.29 +if term2str res = "c * (x ^^^ 3 / 3) + c_2 * x" then () else error "Integral c * x ^^^ 2 + c_2 D x";
4.30 +
4.31 +val rls = add_new_c;
4.32 +val t = (Thm.term_of o the o (parse thy)) "c * (x ^^^ 3 / 3) + c_2 * x";
4.33 +val SOME (res, _) = rewrite_set_inst_ thy true subs rls t;
4.34 +if term2str res = "c * (x ^^^ 3 / 3) + c_2 * x + c_3" then ()
4.35 else error "integrate.sml: diff.behav. in add_new_c simpl.";
4.36
4.37 -val str = rewrit_sinst subs' rls "F x = x ^^^ 3 / 3 + x";
4.38 -if str = "F x = x ^^^ 3 / 3 + x + c"(*not "F x + c =..."*) then ()
4.39 +val t = (Thm.term_of o the o (parse thy)) "F x = x ^^^ 3 / 3 + x";
4.40 +val SOME (res, _) = rewrite_set_inst_ thy true subs rls t;
4.41 +if term2str res = "F x = x ^^^ 3 / 3 + x + c"(*not "F x + c =..."*) then ()
4.42 else error "integrate.sml: diff.behav. in add_new_c equation";
4.43
4.44 -val rls = "simplify_Integral";
4.45 +val rls = simplify_Integral;
4.46 (*~~~~~~~~~~~~~~~~~~~~~~~~~~~*)
4.47 -val str = "ff x = c * x + -1 * q_0 * (x ^^^ 2 / 2) + c_2";
4.48 -val str = rewrit_sinst subs' rls str;
4.49 -if str = "ff x = c_2 + c * x + -1 * q_0 / 2 * x ^^^ 2"
4.50 +val t = (Thm.term_of o the o (parse thy)) "ff x = c * x + -1 * q_0 * (x ^^^ 2 / 2) + c_2";
4.51 +val SOME (res, _) = rewrite_set_inst_ thy true subs rls t;
4.52 +if term2str res = "ff x = c_2 + c * x + -1 * q_0 / 2 * x ^^^ 2"
4.53 then () else error "integrate.sml: diff.behav. in simplify_I #1";
4.54
4.55 -val rls = "integration";
4.56 +val rls = integration;
4.57 (*~~~~~~~~~~~~~~~~~~~~~~~~~~~*)
4.58 -val str = rewrit_sinst subs' rls "Integral c * x ^^^ 2 + c_2 D x";
4.59 -if str = "c_3 + c_2 * x + c / 3 * x ^^^ 3"
4.60 +val t = (Thm.term_of o the o (parse thy)) "Integral c * x ^^^ 2 + c_2 D x";
4.61 +val SOME (res, _) = rewrite_set_inst_ thy true subs rls t;
4.62 +if term2str res = "c_3 + c_2 * x + c / 3 * x ^^^ 3"
4.63 then () else error "integrate.sml: diff.behav. in integration #1";
4.64
4.65 -val str = rewrit_sinst subs' rls "Integral 3*x^^^2 + 2*x + 1 D x";
4.66 -if str = "c + x + x ^^^ 2 + x ^^^ 3" then ()
4.67 +val t = (Thm.term_of o the o (parse thy)) "Integral 3*x^^^2 + 2*x + 1 D x";
4.68 +val SOME (res, _) = rewrite_set_inst_ thy true subs rls t;
4.69 +if term2str res = "c + x + x ^^^ 2 + x ^^^ 3" then ()
4.70 else error "integrate.sml: diff.behav. in integration #2";
4.71
4.72 -val str = rewrit_sinst subs' rls
4.73 +val t = (Thm.term_of o the o (parse thy))
4.74 + "Integral 1 / EI * (L * q_0 / 2 * x + -1 * q_0 / 2 * x ^^^ 2) D x";
4.75 +val SOME (res, _) = rewrite_set_inst_ thy true subs rls t;
4.76 "Integral 1 / EI * (L * q_0 / 2 * x + -1 * q_0 / 2 * x ^^^ 2) D x";
4.77 -if str =
4.78 - "c + 1 / EI * (L * q_0 / 4 * x ^^^ 2 + -1 * q_0 / 6 * x ^^^ 3)"
4.79 +if term2str res = "c + 1 / EI * (L * q_0 / 4 * x ^^^ 2 + -1 * q_0 / 6 * x ^^^ 3)"
4.80 then () else error "integrate.sml: diff.behav. in integration #3";
4.81
4.82 -val str = "Integral "^str^" D x";
4.83 -val str = rewrit_sinst subs' rls str;
4.84 -if str =
4.85 - "c_2 + c * x + 1 / EI * (L * q_0 / 12 * x ^^^ 3 + -1 * q_0 / 24 * x ^^^ 4)"
4.86 +val t = (Thm.term_of o the o (parse thy)) ("Integral " ^ term2str res ^ " D x");
4.87 +val SOME (res, _) = rewrite_set_inst_ thy true subs rls t;
4.88 +if term2str res = "c_2 + c * x + 1 / EI * (L * q_0 / 12 * x ^^^ 3 + -1 * q_0 / 24 * x ^^^ 4)"
4.89 then () else error "integrate.sml: diff.behav. in integration #4";
4.90
4.91 -
4.92 "----------- rewrite 3rd integration in 7.27 ------------";
4.93 "----------- rewrite 3rd integration in 7.27 ------------";
4.94 "----------- rewrite 3rd integration in 7.27 ------------";
5.1 --- a/test/Tools/isac/ProgLang/calculate.sml Sun Feb 25 07:13:47 2018 +0100
5.2 +++ b/test/Tools/isac/ProgLang/calculate.sml Sun Feb 25 10:19:18 2018 +0100
5.3 @@ -153,41 +153,24 @@
5.4 (*-------------- eval_cancel works: *)
5.5 trace_rewrite:=false;
5.6 val thy = @{theory Test};
5.7 + val rls = Test_simplify;
5.8 val t = (Thm.term_of o the o (parse thy)) "(-4) / 2";
5.9
5.10 val SOME (_, t) = eval_cancel "xxx" "Rings.divide_class.divide" t thy;
5.11
5.12 (*--------------(5): reproduce (1) with simpler term: ------------*)
5.13 - val thy = "Test";
5.14 - val t = "(3+5)/2";
5.15 - val (t,_) = the (rewrite_set thy false rls t);
5.16 -(*val t = "4" ... works*)
5.17 + val t = (Thm.term_of o the o (parse thy)) "(3+5)/2";
5.18 +case rewrite_set_ thy false rls t of
5.19 + SOME (Free ("4", _), []) => ()
5.20 +| _ => error "rewrite_set_ (3+5)/2 changed";
5.21
5.22 - val t = "(3+1+2*x)/2";
5.23 - val (t,_) = the (rewrite_set thy false rls t);
5.24 -(*val t = "2 + x" ... works*)
5.25 + val t = (Thm.term_of o the o (parse thy)) "(3+1+2*x)/2";
5.26 +case rewrite_set_ thy false rls t of
5.27 + SOME (Const ("Groups.plus_class.plus", _) $ Free ("2", _) $ Free ("x", _), []) => ()
5.28 +| _ => error "rewrite_set_ (3+1+2*x)/2 changed";
5.29
5.30 trace_rewrite:=false; (*=true3.6.03*)
5.31
5.32 - val thy = "Test";
5.33 - val rls = "Test_simplify";
5.34 - val t = "(3+(1+2*x))/2";
5.35 - val (t,_) = the (rewrite_set thy false rls t);
5.36 -(*val t = "2 + x" ... works: give up----------------------------------------*)
5.37 - trace_rewrite:=false;
5.38 -
5.39 - trace_rewrite:=false; (*=true3.6.03*)
5.40 - val thy = @{theory Test};
5.41 - val rls = Test_simplify;
5.42 - val t = str2term "(3+(1+2*x))/2";
5.43 - val SOME (t',asm) = rewrite_set_ thy false rls t;
5.44 - term2str t';
5.45 -(*val t = "2 + x" ... works: give up----------------------------------------*)
5.46 - trace_rewrite:=false;
5.47 -
5.48 -
5.49 -
5.50 -
5.51 (*--- trace_rewrite before correction of ... --------------------
5.52 val ct = "(-3 + 2 * x + -1) / 2";
5.53 val (ct,_) = the (rewrite_set thy' false rls ct);
5.54 @@ -218,10 +201,9 @@
5.55
5.56 (*===================*)
5.57 trace_rewrite:=false; (*WN130722: =true stopped Test_Isac.thy*)
5.58 - val thy' = "Test";
5.59 - val rls = "Test_simplify";
5.60 - val ct = "x + (-1 + -3) / 2";
5.61 - val (ct,_) = the (rewrite_set thy' false rls ct);
5.62 + val t = (Thm.term_of o the o (parse thy)) "x + (-1 + -3) / 2";
5.63 +val SOME (res, []) = rewrite_set_ thy false rls t;
5.64 +if term2str res = "-2 + x" then () else error "rewrite_set_ x + (-1 + -3) / 2 changed";
5.65 "x + (-4) / 2";
5.66 (*
5.67 ### trying calc. 'cancel'
5.68 @@ -237,23 +219,6 @@
5.69 *)
5.70
5.71 trace_rewrite:=false; (*WN130722: =true stopped Test_Isac.thy*)
5.72 - val thy' = "Test";
5.73 - val rls = "Test_simplify";
5.74 - val ct = "x + (-4) / 2";
5.75 - val (ct,_) = the (rewrite_set thy' false rls ct);
5.76 -"(-2) + x";
5.77 -(*
5.78 -### trying calc. 'cancel'
5.79 -@@@ get_pair: binop, t = x + -4 / 2
5.80 -@@@ get_pair: t else
5.81 -@@@ get_pair: t else -> NONE
5.82 -@@@ get_pair: binop, t = -4 / 2
5.83 -@@@ get_pair: then 1
5.84 -@@@ adhoc_thm': SOME #cancel_-4_2
5.85 -### calc. to: x + (-2)
5.86 -### trying calc. 'cancel'
5.87 -*)
5.88 - trace_rewrite:=false;
5.89
5.90 "----------- Atools.pow Power.power_class.power ---------";
5.91 "----------- Atools.pow Power.power_class.power ---------";
6.1 --- a/test/Tools/isac/Test_Isac.thy Sun Feb 25 07:13:47 2018 +0100
6.2 +++ b/test/Tools/isac/Test_Isac.thy Sun Feb 25 10:19:18 2018 +0100
6.3 @@ -102,7 +102,8 @@
6.4 open Stool; transfer_asms_from_to;
6.5 open Tac; (* NONE *)
6.6 open Model; (* NONE *)
6.7 - open LTool; (* NONE *)
6.8 + open LTool; rule2stac;
6.9 + open Rewrite; mk_thm;
6.10 (*\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
6.11 *}
6.12