1.1 --- a/src/Tools/isac/Knowledge/PolyEq.thy Sat Jun 22 14:34:06 2019 +0200
1.2 +++ b/src/Tools/isac/Knowledge/PolyEq.thy Sun Jun 23 14:23:09 2019 +0200
1.3 @@ -385,7 +385,7 @@
1.4 Rule.Thm ("cancel_leading_coeff11",TermC.num_str @{thm cancel_leading_coeff11}),
1.5 Rule.Thm ("cancel_leading_coeff12",TermC.num_str @{thm cancel_leading_coeff12}),
1.6 Rule.Thm ("cancel_leading_coeff13",TermC.num_str @{thm cancel_leading_coeff13})
1.7 - ],scr = Rule.Prog ((Thm.term_of o the o (TermC.parse thy)) "empty_script")});
1.8 + ],scr = Rule.EmptyScr});
1.9
1.10 val prep_rls' = LTool.prep_rls @{theory};
1.11 \<close>
1.12 @@ -400,7 +400,7 @@
1.13 Rule.Thm ("complete_square4",TermC.num_str @{thm complete_square4}),
1.14 Rule.Thm ("complete_square5",TermC.num_str @{thm complete_square5})
1.15 ],
1.16 - scr = Rule.Prog ((Thm.term_of o the o (TermC.parse thy)) "empty_script")
1.17 + scr = Rule.EmptyScr
1.18 });
1.19
1.20 val polyeq_simplify = prep_rls'(
1.21 @@ -422,7 +422,7 @@
1.22 Rule.Calc ("Atools.pow" ,eval_binop "#power_"),
1.23 Rule.Rls_ reduce_012
1.24 ],
1.25 - scr = Rule.Prog ((Thm.term_of o the o (TermC.parse thy)) "empty_script")
1.26 + scr = Rule.EmptyScr
1.27 });
1.28 \<close>
1.29 setup \<open>KEStore_Elems.add_rlss
1.30 @@ -444,7 +444,7 @@
1.31 rules = [Rule.Thm("d0_true",TermC.num_str @{thm d0_true}),
1.32 Rule.Thm("d0_false",TermC.num_str @{thm d0_false})
1.33 ],
1.34 - scr = Rule.Prog ((Thm.term_of o the o (TermC.parse thy)) "empty_script")
1.35 + scr = Rule.EmptyScr
1.36 });
1.37
1.38 (* -- d1 -- *)
1.39 @@ -463,7 +463,7 @@
1.40 Rule.Thm("d1_isolate_div",TermC.num_str @{thm d1_isolate_div})
1.41 (* bx=c -> x=c/b *)
1.42 ],
1.43 - scr = Rule.Prog ((Thm.term_of o the o (TermC.parse thy)) "empty_script")
1.44 + scr = Rule.EmptyScr
1.45 });
1.46
1.47 \<close>
1.48 @@ -486,7 +486,7 @@
1.49 Rule.Thm ("d2_reduce_equation2", TermC.num_str @{thm d2_reduce_equation2}),(* x(a+ x)=0 -> x=0 |a+ x=0*)
1.50 Rule.Thm ("d2_isolate_div", TermC.num_str @{thm d2_isolate_div}) (* bx^2=c -> x^2=c/b *)
1.51 ],
1.52 - scr = Rule.Prog ((Thm.term_of o the o (TermC.parse thy)) "empty_script")
1.53 + scr = Rule.EmptyScr
1.54 });
1.55 \<close>
1.56 ML\<open>
1.57 @@ -513,7 +513,7 @@
1.58 Rule.Thm("d2_isolate_div",TermC.num_str @{thm d2_isolate_div})
1.59 (* bx^2=c -> x^2=c/b*)
1.60 ],
1.61 - scr = Rule.Prog ((Thm.term_of o the o (TermC.parse thy)) "empty_script")
1.62 + scr = Rule.EmptyScr
1.63 });
1.64 \<close>
1.65 ML\<open>
1.66 @@ -559,7 +559,7 @@
1.67 (* x^2=0 *)
1.68 Rule.Thm("d2_sqrt_equation3",TermC.num_str @{thm d2_sqrt_equation3})
1.69 (* 1x^2=0 *)
1.70 - ],scr = Rule.Prog ((Thm.term_of o the o (TermC.parse thy)) "empty_script")
1.71 + ],scr = Rule.EmptyScr
1.72 });
1.73 \<close>
1.74 ML\<open>
1.75 @@ -606,7 +606,7 @@
1.76 Rule.Thm("d2_sqrt_equation3",TermC.num_str @{thm d2_sqrt_equation3})
1.77 (* bx^2=0 *)
1.78 ],
1.79 - scr = Rule.Prog ((Thm.term_of o the o (TermC.parse thy)) "empty_script")
1.80 + scr = Rule.EmptyScr
1.81 });
1.82 \<close>
1.83 ML\<open>
1.84 @@ -666,7 +666,7 @@
1.85 Rule.Thm("d2_isolate_div",TermC.num_str @{thm d2_isolate_div})
1.86 (* bx^2=c -> x^2=c/b*)
1.87 ],
1.88 - scr = Rule.Prog ((Thm.term_of o the o (TermC.parse thy)) "empty_script")
1.89 + scr = Rule.EmptyScr
1.90 });
1.91 \<close>
1.92 ML\<open>
1.93 @@ -739,7 +739,7 @@
1.94 Rule.Thm("d3_root_equation1",TermC.num_str @{thm d3_root_equation1})
1.95 (*bdv^^^3=c) = (bdv = nroot 3 c*)
1.96 ],
1.97 - scr = Rule.Prog ((Thm.term_of o the o (TermC.parse thy)) "empty_script")
1.98 + scr = Rule.EmptyScr
1.99 });
1.100 \<close>
1.101 ML\<open>
1.102 @@ -754,7 +754,7 @@
1.103 [Rule.Thm("d4_sub_u1",TermC.num_str @{thm d4_sub_u1})
1.104 (* ax^4+bx^2+c=0 -> x=+-sqrt(ax^2+bx^+c) *)
1.105 ],
1.106 - scr = Rule.Prog ((Thm.term_of o the o (TermC.parse thy)) "empty_script")
1.107 + scr = Rule.EmptyScr
1.108 });
1.109 \<close>
1.110 setup \<open>KEStore_Elems.add_rlss