1.1 --- a/src/Tools/isac/Knowledge/EqSystem.thy Wed Apr 01 19:20:05 2020 +0200
1.2 +++ b/src/Tools/isac/Knowledge/EqSystem.thy Sat Apr 04 12:11:32 2020 +0200
1.3 @@ -170,10 +170,10 @@
1.4
1.5 (*.adapted from 'order_add_mult_in' by just replacing the rew_ord.*)
1.6 val order_add_mult_System =
1.7 - Rule.Rls{id = "order_add_mult_System", preconds = [],
1.8 + Rule_Set.Rls{id = "order_add_mult_System", preconds = [],
1.9 rew_ord = ("ord_simplify_System",
1.10 ord_simplify_System false @{theory "Integrate"}),
1.11 - erls = Rule.e_rls,srls = Rule.Erls, calc = [], errpatts = [],
1.12 + erls = Rule_Set.e_rls,srls = Rule_Set.Erls, calc = [], errpatts = [],
1.13 rules = [Rule.Thm ("mult_commute",TermC.num_str @{thm mult.commute}),
1.14 (* z * w = w * z *)
1.15 Rule.Thm ("real_mult_left_commute",TermC.num_str @{thm real_mult_left_commute}),
1.16 @@ -194,9 +194,9 @@
1.17 #1 using 'ord_simplify_System' in 'order_add_mult_System'
1.18 #2 NOT using common_nominator_p .*)
1.19 val norm_System_noadd_fractions =
1.20 - Rule.Rls {id = "norm_System_noadd_fractions", preconds = [],
1.21 + Rule_Set.Rls {id = "norm_System_noadd_fractions", preconds = [],
1.22 rew_ord = ("dummy_ord",Rule.dummy_ord),
1.23 - erls = norm_rat_erls, srls = Rule.Erls, calc = [], errpatts = [],
1.24 + erls = norm_rat_erls, srls = Rule_Set.Erls, calc = [], errpatts = [],
1.25 rules = [(*sequence given by operator precedence*)
1.26 Rule.Rls_ discard_minus,
1.27 Rule.Rls_ powers,
1.28 @@ -215,9 +215,9 @@
1.29 (*.adapted from 'norm_Rational' by
1.30 *1* using 'ord_simplify_System' in 'order_add_mult_System'.*)
1.31 val norm_System =
1.32 - Rule.Rls {id = "norm_System", preconds = [],
1.33 + Rule_Set.Rls {id = "norm_System", preconds = [],
1.34 rew_ord = ("dummy_ord",Rule.dummy_ord),
1.35 - erls = norm_rat_erls, srls = Rule.Erls, calc = [], errpatts = [],
1.36 + erls = norm_rat_erls, srls = Rule_Set.Erls, calc = [], errpatts = [],
1.37 rules = [(*sequence given by operator precedence*)
1.38 Rule.Rls_ discard_minus,
1.39 Rule.Rls_ powers,
1.40 @@ -243,9 +243,9 @@
1.41 *3* discard_parentheses only for (.*(.*.))
1.42 analoguous to simplify_Integral .*)
1.43 val simplify_System_parenthesized =
1.44 - Rule.Seq {id = "simplify_System_parenthesized", preconds = []:term list,
1.45 + Rule_Set.Seq {id = "simplify_System_parenthesized", preconds = []:term list,
1.46 rew_ord = ("dummy_ord", Rule.dummy_ord),
1.47 - erls = Atools_erls, srls = Rule.Erls, calc = [], errpatts = [],
1.48 + erls = Atools_erls, srls = Rule_Set.Erls, calc = [], errpatts = [],
1.49 rules = [Rule.Thm ("distrib_right",TermC.num_str @{thm distrib_right}),
1.50 (*"(?z1.0 + ?z2.0) * ?w = ?z1.0 * ?w + ?z2.0 * ?w"*)
1.51 Rule.Thm ("add_divide_distrib",TermC.num_str @{thm add_divide_distrib}),
1.52 @@ -268,9 +268,9 @@
1.53 *1* ord_simplify_System instead of termlessI .*)
1.54 (*TODO.WN051031 ^^^^^^^^^^ should be in EACH rls contained *)
1.55 val simplify_System =
1.56 - Rule.Seq {id = "simplify_System", preconds = []:term list,
1.57 + Rule_Set.Seq {id = "simplify_System", preconds = []:term list,
1.58 rew_ord = ("dummy_ord", Rule.dummy_ord),
1.59 - erls = Atools_erls, srls = Rule.Erls, calc = [], errpatts = [],
1.60 + erls = Atools_erls, srls = Rule_Set.Erls, calc = [], errpatts = [],
1.61 rules = [Rule.Rls_ norm_Rational,
1.62 Rule.Rls_ (*order_add_mult_in*) norm_System (**1**),
1.63 Rule.Rls_ discard_parentheses,
1.64 @@ -281,21 +281,21 @@
1.65 scr = Rule.EmptyScr};
1.66 (*
1.67 val simplify_System =
1.68 - Rule.append_rls "simplify_System" simplify_System_parenthesized
1.69 + Rule_Set.append_rls "simplify_System" simplify_System_parenthesized
1.70 [Rule.Thm ("sym_add_assoc",
1.71 TermC.num_str (@{thm add.assoc} RS @{thm sym}))];
1.72 *)
1.73 \<close>
1.74 ML \<open>
1.75 val isolate_bdvs =
1.76 - Rule.Rls {id="isolate_bdvs", preconds = [],
1.77 + Rule_Set.Rls {id="isolate_bdvs", preconds = [],
1.78 rew_ord = ("e_rew_ord", Rule.e_rew_ord),
1.79 - erls = Rule.append_rls "erls_isolate_bdvs" Rule.e_rls
1.80 + erls = Rule_Set.append_rls "erls_isolate_bdvs" Rule_Set.e_rls
1.81 [(Rule.Num_Calc ("EqSystem.occur'_exactly'_in",
1.82 eval_occur_exactly_in
1.83 "#eval_occur_exactly_in_"))
1.84 ],
1.85 - srls = Rule.Erls, calc = [], errpatts = [],
1.86 + srls = Rule_Set.Erls, calc = [], errpatts = [],
1.87 rules =
1.88 [Rule.Thm ("commute_0_equality", TermC.num_str @{thm commute_0_equality}),
1.89 Rule.Thm ("separate_bdvs_add", TermC.num_str @{thm separate_bdvs_add}),
1.90 @@ -304,10 +304,10 @@
1.91 \<close>
1.92 ML \<open>
1.93 val isolate_bdvs_4x4 =
1.94 - Rule.Rls {id="isolate_bdvs_4x4", preconds = [],
1.95 + Rule_Set.Rls {id="isolate_bdvs_4x4", preconds = [],
1.96 rew_ord = ("e_rew_ord", Rule.e_rew_ord),
1.97 - erls = Rule.append_rls
1.98 - "erls_isolate_bdvs_4x4" Rule.e_rls
1.99 + erls = Rule_Set.append_rls
1.100 + "erls_isolate_bdvs_4x4" Rule_Set.e_rls
1.101 [Rule.Num_Calc ("EqSystem.occur'_exactly'_in",
1.102 eval_occur_exactly_in "#eval_occur_exactly_in_"),
1.103 Rule.Num_Calc ("Prog_Expr.ident", Prog_Expr.eval_ident "#ident_"),
1.104 @@ -315,7 +315,7 @@
1.105 Rule.Thm ("not_true",TermC.num_str @{thm not_true}),
1.106 Rule.Thm ("not_false",TermC.num_str @{thm not_false})
1.107 ],
1.108 - srls = Rule.Erls, calc = [], errpatts = [],
1.109 + srls = Rule_Set.Erls, calc = [], errpatts = [],
1.110 rules = [Rule.Thm ("commute_0_equality", TermC.num_str @{thm commute_0_equality}),
1.111 Rule.Thm ("separate_bdvs0", TermC.num_str @{thm separate_bdvs0}),
1.112 Rule.Thm ("separate_bdvs_add1", TermC.num_str @{thm separate_bdvs_add1}),
1.113 @@ -329,20 +329,20 @@
1.114 (*.order the equations in a system such, that a triangular system (if any)
1.115 appears as [..c_4 = .., ..., ..., ..c_1 + ..c_2 + ..c_3 ..c_4 = ..].*)
1.116 val order_system =
1.117 - Rule.Rls {id="order_system", preconds = [],
1.118 + Rule_Set.Rls {id="order_system", preconds = [],
1.119 rew_ord = ("ord_simplify_System",
1.120 ord_simplify_System false thy),
1.121 - erls = Rule.Erls, srls = Rule.Erls, calc = [], errpatts = [],
1.122 + erls = Rule_Set.Erls, srls = Rule_Set.Erls, calc = [], errpatts = [],
1.123 rules = [Rule.Thm ("order_system_NxN", TermC.num_str @{thm order_system_NxN})
1.124 ],
1.125 scr = Rule.EmptyScr};
1.126
1.127 val prls_triangular =
1.128 - Rule.Rls {id="prls_triangular", preconds = [],
1.129 + Rule_Set.Rls {id="prls_triangular", preconds = [],
1.130 rew_ord = ("e_rew_ord", Rule.e_rew_ord),
1.131 - erls = Rule.Rls {id="erls_prls_triangular", preconds = [],
1.132 + erls = Rule_Set.Rls {id="erls_prls_triangular", preconds = [],
1.133 rew_ord = ("e_rew_ord", Rule.e_rew_ord),
1.134 - erls = Rule.Erls, srls = Rule.Erls, calc = [], errpatts = [],
1.135 + erls = Rule_Set.Erls, srls = Rule_Set.Erls, calc = [], errpatts = [],
1.136 rules = [(*for precond NTH_CONS ...*)
1.137 Rule.Num_Calc ("Orderings.ord_class.less", Prog_Expr.eval_equ "#less_"),
1.138 Rule.Num_Calc ("Groups.plus_class.plus", (**)eval_binop "#add_")
1.139 @@ -350,7 +350,7 @@
1.140 '+' into precondition !*)
1.141 ],
1.142 scr = Rule.EmptyScr},
1.143 - srls = Rule.Erls, calc = [], errpatts = [],
1.144 + srls = Rule_Set.Erls, calc = [], errpatts = [],
1.145 rules = [Rule.Thm ("NTH_CONS",TermC.num_str @{thm NTH_CONS}),
1.146 Rule.Num_Calc ("Groups.plus_class.plus", (**)eval_binop "#add_"),
1.147 Rule.Thm ("NTH_NIL",TermC.num_str @{thm NTH_NIL}),
1.148 @@ -367,11 +367,11 @@
1.149 (*WN060914 quickly created for 4x4;
1.150 more similarity to prls_triangular desirable*)
1.151 val prls_triangular4 =
1.152 - Rule.Rls {id="prls_triangular4", preconds = [],
1.153 + Rule_Set.Rls {id="prls_triangular4", preconds = [],
1.154 rew_ord = ("e_rew_ord", Rule.e_rew_ord),
1.155 - erls = Rule.Rls {id="erls_prls_triangular4", preconds = [],
1.156 + erls = Rule_Set.Rls {id="erls_prls_triangular4", preconds = [],
1.157 rew_ord = ("e_rew_ord", Rule.e_rew_ord),
1.158 - erls = Rule.Erls, srls = Rule.Erls, calc = [], errpatts = [],
1.159 + erls = Rule_Set.Erls, srls = Rule_Set.Erls, calc = [], errpatts = [],
1.160 rules = [(*for precond NTH_CONS ...*)
1.161 Rule.Num_Calc ("Orderings.ord_class.less", Prog_Expr.eval_equ "#less_"),
1.162 Rule.Num_Calc ("Groups.plus_class.plus", (**)eval_binop "#add_")
1.163 @@ -379,7 +379,7 @@
1.164 '+' into precondition !*)
1.165 ],
1.166 scr = Rule.EmptyScr},
1.167 - srls = Rule.Erls, calc = [], errpatts = [],
1.168 + srls = Rule_Set.Erls, calc = [], errpatts = [],
1.169 rules = [Rule.Thm ("NTH_CONS",TermC.num_str @{thm NTH_CONS}),
1.170 Rule.Num_Calc ("Groups.plus_class.plus", (**)eval_binop "#add_"),
1.171 Rule.Thm ("NTH_NIL",TermC.num_str @{thm NTH_NIL}),
1.172 @@ -410,20 +410,20 @@
1.173 (["system"],
1.174 [("#Given" ,["equalities e_s", "solveForVars v_s"]),
1.175 ("#Find" ,["solution ss'''"](*''' is copy-named*))],
1.176 - Rule.append_rls "e_rls" Rule.e_rls [(*for preds in where_*)], SOME "solveSystem e_s v_s", [])),
1.177 + Rule_Set.append_rls "e_rls" Rule_Set.e_rls [(*for preds in where_*)], SOME "solveSystem e_s v_s", [])),
1.178 (Specify.prep_pbt thy "pbl_equsys_lin" [] Celem.e_pblID
1.179 (["LINEAR", "system"],
1.180 [("#Given" ,["equalities e_s", "solveForVars v_s"]),
1.181 (*TODO.WN050929 check linearity*)
1.182 ("#Find" ,["solution ss'''"])],
1.183 - Rule.append_rls "e_rls" Rule.e_rls [(*for preds in where_*)], SOME "solveSystem e_s v_s", [])),
1.184 + Rule_Set.append_rls "e_rls" Rule_Set.e_rls [(*for preds in where_*)], SOME "solveSystem e_s v_s", [])),
1.185 (Specify.prep_pbt thy "pbl_equsys_lin_2x2" [] Celem.e_pblID
1.186 (["2x2", "LINEAR", "system"],
1.187 (*~~~~~~~~~~~~~~~~~~~~~~~~~*)
1.188 [("#Given" ,["equalities e_s", "solveForVars v_s"]),
1.189 ("#Where" ,["LENGTH (e_s:: bool list) = 2", "LENGTH v_s = 2"]),
1.190 ("#Find" ,["solution ss'''"])],
1.191 - Rule.append_rls "prls_2x2_linear_system" Rule.e_rls
1.192 + Rule_Set.append_rls "prls_2x2_linear_system" Rule_Set.e_rls
1.193 [Rule.Thm ("LENGTH_CONS",TermC.num_str @{thm LENGTH_CONS}),
1.194 Rule.Thm ("LENGTH_NIL",TermC.num_str @{thm LENGTH_NIL}),
1.195 Rule.Num_Calc ("Groups.plus_class.plus", (**)eval_binop "#add_"),
1.196 @@ -441,7 +441,7 @@
1.197 (["normalise", "2x2", "LINEAR", "system"],
1.198 [("#Given" ,["equalities e_s", "solveForVars v_s"]),
1.199 ("#Find" ,["solution ss'''"])],
1.200 - Rule.append_rls "e_rls" Rule.e_rls [(*for preds in where_*)],
1.201 + Rule_Set.append_rls "e_rls" Rule_Set.e_rls [(*for preds in where_*)],
1.202 SOME "solveSystem e_s v_s",
1.203 [["EqSystem","normalise","2x2"]])),
1.204 (Specify.prep_pbt thy "pbl_equsys_lin_3x3" [] Celem.e_pblID
1.205 @@ -450,7 +450,7 @@
1.206 [("#Given" ,["equalities e_s", "solveForVars v_s"]),
1.207 ("#Where" ,["LENGTH (e_s:: bool list) = 3", "LENGTH v_s = 3"]),
1.208 ("#Find" ,["solution ss'''"])],
1.209 - Rule.append_rls "prls_3x3_linear_system" Rule.e_rls
1.210 + Rule_Set.append_rls "prls_3x3_linear_system" Rule_Set.e_rls
1.211 [Rule.Thm ("LENGTH_CONS",TermC.num_str @{thm LENGTH_CONS}),
1.212 Rule.Thm ("LENGTH_NIL",TermC.num_str @{thm LENGTH_NIL}),
1.213 Rule.Num_Calc ("Groups.plus_class.plus", (**)eval_binop "#add_"),
1.214 @@ -462,7 +462,7 @@
1.215 [("#Given" ,["equalities e_s", "solveForVars v_s"]),
1.216 ("#Where" ,["LENGTH (e_s:: bool list) = 4", "LENGTH v_s = 4"]),
1.217 ("#Find" ,["solution ss'''"])],
1.218 - Rule.append_rls "prls_4x4_linear_system" Rule.e_rls
1.219 + Rule_Set.append_rls "prls_4x4_linear_system" Rule_Set.e_rls
1.220 [Rule.Thm ("LENGTH_CONS",TermC.num_str @{thm LENGTH_CONS}),
1.221 Rule.Thm ("LENGTH_NIL",TermC.num_str @{thm LENGTH_NIL}),
1.222 Rule.Num_Calc ("Groups.plus_class.plus", (**)eval_binop "#add_"),
1.223 @@ -477,7 +477,7 @@
1.224 "(NTH 3 (v_s::real list)) occurs_in (NTH 3 (e_s::bool list))",
1.225 "(NTH 4 (v_s::real list)) occurs_in (NTH 4 (e_s::bool list))"]),
1.226 ("#Find" ,["solution ss'''"])],
1.227 - Rule.append_rls "prls_tri_4x4_lin_sys" prls_triangular
1.228 + Rule_Set.append_rls "prls_tri_4x4_lin_sys" prls_triangular
1.229 [Rule.Num_Calc ("Prog_Expr.occurs'_in", Prog_Expr.eval_occurs_in "")],
1.230 SOME "solveSystem e_s v_s",
1.231 [["EqSystem","top_down_substitution","4x4"]])),
1.232 @@ -486,22 +486,22 @@
1.233 [("#Given" ,["equalities e_s", "solveForVars v_s"]),
1.234 (*LENGTH is checked 1 level above*)
1.235 ("#Find" ,["solution ss'''"])],
1.236 - Rule.append_rls "e_rls" Rule.e_rls [(*for preds in where_*)],
1.237 + Rule_Set.append_rls "e_rls" Rule_Set.e_rls [(*for preds in where_*)],
1.238 SOME "solveSystem e_s v_s",
1.239 [["EqSystem","normalise","4x4"]]))]\<close>
1.240
1.241 ML \<open>
1.242 (*this is for NTH only*)
1.243 -val srls = Rule.Rls {id="srls_normalise_4x4",
1.244 +val srls = Rule_Set.Rls {id="srls_normalise_4x4",
1.245 preconds = [],
1.246 rew_ord = ("termlessI",termlessI),
1.247 - erls = Rule.append_rls "erls_in_srls_IntegrierenUnd.." Rule.e_rls
1.248 + erls = Rule_Set.append_rls "erls_in_srls_IntegrierenUnd.." Rule_Set.e_rls
1.249 [(*for asm in NTH_CONS ...*)
1.250 Rule.Num_Calc ("Orderings.ord_class.less", Prog_Expr.eval_equ "#less_"),
1.251 (*2nd NTH_CONS pushes n+-1 into asms*)
1.252 Rule.Num_Calc("Groups.plus_class.plus", (**)eval_binop "#add_")
1.253 ],
1.254 - srls = Rule.Erls, calc = [], errpatts = [],
1.255 + srls = Rule_Set.Erls, calc = [], errpatts = [],
1.256 rules = [Rule.Thm ("NTH_CONS",TermC.num_str @{thm NTH_CONS}),
1.257 Rule.Num_Calc("Groups.plus_class.plus", (**)eval_binop "#add_"),
1.258 Rule.Thm ("NTH_NIL",TermC.num_str @{thm NTH_NIL})],
1.259 @@ -512,13 +512,13 @@
1.260 setup \<open>KEStore_Elems.add_mets
1.261 [Specify.prep_met thy "met_eqsys" [] Celem.e_metID
1.262 (["EqSystem"], [],
1.263 - {rew_ord'="tless_true", rls' = Rule.Erls, calc = [], srls = Rule.Erls, prls = Rule.Erls, crls = Rule.Erls,
1.264 - errpats = [], nrls = Rule.Erls},
1.265 + {rew_ord'="tless_true", rls' = Rule_Set.Erls, calc = [], srls = Rule_Set.Erls, prls = Rule_Set.Erls, crls = Rule_Set.Erls,
1.266 + errpats = [], nrls = Rule_Set.Erls},
1.267 @{thm refl}),
1.268 Specify.prep_met thy "met_eqsys_topdown" [] Celem.e_metID
1.269 (["EqSystem","top_down_substitution"], [],
1.270 - {rew_ord'="tless_true", rls' = Rule.Erls, calc = [], srls = Rule.Erls, prls = Rule.Erls, crls = Rule.Erls,
1.271 - errpats = [], nrls = Rule.Erls},
1.272 + {rew_ord'="tless_true", rls' = Rule_Set.Erls, calc = [], srls = Rule_Set.Erls, prls = Rule_Set.Erls, crls = Rule_Set.Erls,
1.273 + errpats = [], nrls = Rule_Set.Erls},
1.274 @{thm refl})]
1.275 \<close>
1.276
1.277 @@ -549,19 +549,19 @@
1.278 ["(tl v_s) from v_s occur_exactly_in (NTH 1 (e_s::bool list))",
1.279 " v_s from v_s occur_exactly_in (NTH 2 (e_s::bool list))"]),
1.280 ("#Find" ,["solution ss'''"])],
1.281 - {rew_ord'="ord_simplify_System", rls' = Rule.Erls, calc = [],
1.282 - srls = Rule.append_rls "srls_top_down_2x2" Rule.e_rls
1.283 + {rew_ord'="ord_simplify_System", rls' = Rule_Set.Erls, calc = [],
1.284 + srls = Rule_Set.append_rls "srls_top_down_2x2" Rule_Set.e_rls
1.285 [Rule.Thm ("hd_thm",TermC.num_str @{thm hd_thm}),
1.286 Rule.Thm ("tl_Cons",TermC.num_str @{thm tl_Cons}),
1.287 Rule.Thm ("tl_Nil",TermC.num_str @{thm tl_Nil})],
1.288 - prls = prls_triangular, crls = Rule.Erls, errpats = [], nrls = Rule.Erls},
1.289 + prls = prls_triangular, crls = Rule_Set.Erls, errpats = [], nrls = Rule_Set.Erls},
1.290 @{thm solve_system.simps})]
1.291 \<close>
1.292 setup \<open>KEStore_Elems.add_mets
1.293 [Specify.prep_met thy "met_eqsys_norm" [] Celem.e_metID
1.294 (["EqSystem", "normalise"], [],
1.295 - {rew_ord'="tless_true", rls' = Rule.Erls, calc = [], srls = Rule.Erls, prls = Rule.Erls, crls = Rule.Erls,
1.296 - errpats = [], nrls = Rule.Erls},
1.297 + {rew_ord'="tless_true", rls' = Rule_Set.Erls, calc = [], srls = Rule_Set.Erls, prls = Rule_Set.Erls, crls = Rule_Set.Erls,
1.298 + errpats = [], nrls = Rule_Set.Erls},
1.299 @{thm refl})]
1.300 \<close>
1.301
1.302 @@ -584,12 +584,12 @@
1.303 (["EqSystem","normalise","2x2"],
1.304 [("#Given" ,["equalities e_s", "solveForVars v_s"]),
1.305 ("#Find" ,["solution ss'''"])],
1.306 - {rew_ord'="tless_true", rls' = Rule.Erls, calc = [],
1.307 - srls = Rule.append_rls "srls_normalise_2x2" Rule.e_rls
1.308 + {rew_ord'="tless_true", rls' = Rule_Set.Erls, calc = [],
1.309 + srls = Rule_Set.append_rls "srls_normalise_2x2" Rule_Set.e_rls
1.310 [Rule.Thm ("hd_thm",TermC.num_str @{thm hd_thm}),
1.311 Rule.Thm ("tl_Cons",TermC.num_str @{thm tl_Cons}),
1.312 Rule.Thm ("tl_Nil",TermC.num_str @{thm tl_Nil})],
1.313 - prls = Rule.Erls, crls = Rule.Erls, errpats = [], nrls = Rule.Erls},
1.314 + prls = Rule_Set.Erls, crls = Rule_Set.Erls, errpats = [], nrls = Rule_Set.Erls},
1.315 @{thm solve_system2.simps})]
1.316 \<close>
1.317
1.318 @@ -616,12 +616,12 @@
1.319 (["EqSystem","normalise","4x4"],
1.320 [("#Given" ,["equalities e_s", "solveForVars v_s"]),
1.321 ("#Find" ,["solution ss'''"])],
1.322 - {rew_ord'="tless_true", rls' = Rule.Erls, calc = [],
1.323 - srls = Rule.append_rls "srls_normalise_4x4" srls
1.324 + {rew_ord'="tless_true", rls' = Rule_Set.Erls, calc = [],
1.325 + srls = Rule_Set.append_rls "srls_normalise_4x4" srls
1.326 [Rule.Thm ("hd_thm",TermC.num_str @{thm hd_thm}),
1.327 Rule.Thm ("tl_Cons",TermC.num_str @{thm tl_Cons}),
1.328 Rule.Thm ("tl_Nil",TermC.num_str @{thm tl_Nil})],
1.329 - prls = Rule.Erls, crls = Rule.Erls, errpats = [], nrls = Rule.Erls},
1.330 + prls = Rule_Set.Erls, crls = Rule_Set.Erls, errpats = [], nrls = Rule_Set.Erls},
1.331 (*STOPPED.WN06? met ["EqSystem","normalise","4x4"] #>#>#>#>#>#>#>#>#>#>#>#>#>@*)
1.332 @{thm solve_system3.simps})]
1.333 \<close>
1.334 @@ -653,11 +653,11 @@
1.335 "(NTH 3 (v_s::real list)) occurs_in (NTH 3 (e_s::bool list))",
1.336 "(NTH 4 (v_s::real list)) occurs_in (NTH 4 (e_s::bool list))"]),
1.337 ("#Find", ["solution ss'''"])],
1.338 - {rew_ord'="ord_simplify_System", rls' = Rule.Erls, calc = [],
1.339 - srls = Rule.append_rls "srls_top_down_4x4" srls [],
1.340 - prls = Rule.append_rls "prls_tri_4x4_lin_sys" prls_triangular
1.341 + {rew_ord'="ord_simplify_System", rls' = Rule_Set.Erls, calc = [],
1.342 + srls = Rule_Set.append_rls "srls_top_down_4x4" srls [],
1.343 + prls = Rule_Set.append_rls "prls_tri_4x4_lin_sys" prls_triangular
1.344 [Rule.Num_Calc ("Prog_Expr.occurs'_in", Prog_Expr.eval_occurs_in "")],
1.345 - crls = Rule.Erls, errpats = [], nrls = Rule.Erls},
1.346 + crls = Rule_Set.Erls, errpats = [], nrls = Rule_Set.Erls},
1.347 (*FIXXXXME.WN060916: this script works ONLY for exp 7.79 #>#>#>#>#>#>#>#>#>#>*)
1.348 @{thm solve_system4.simps})]
1.349 \<close>