1.1 --- a/src/Tools/isac/Knowledge/EqSystem.thy Mon Aug 09 14:20:20 2021 +0200
1.2 +++ b/src/Tools/isac/Knowledge/EqSystem.thy Tue Aug 10 09:43:07 2021 +0200
1.3 @@ -169,24 +169,18 @@
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_Def.Repeat{id = "order_add_mult_System", preconds = [],
1.8 - rew_ord = ("ord_simplify_System",
1.9 - ord_simplify_System false @{theory "Integrate"}),
1.10 - erls = Rule_Set.empty,srls = Rule_Set.Empty, calc = [], errpatts = [],
1.11 - rules = [\<^rule_thm>\<open>mult.commute\<close>,
1.12 - (* z * w = w * z *)
1.13 - \<^rule_thm>\<open>real_mult_left_commute\<close>,
1.14 - (*z1.0 * (z2.0 * z3.0) = z2.0 * (z1.0 * z3.0)*)
1.15 - \<^rule_thm>\<open>mult.assoc\<close>,
1.16 - (*z1.0 * z2.0 * z3.0 = z1.0 * (z2.0 * z3.0)*)
1.17 - \<^rule_thm>\<open>add.commute\<close>,
1.18 - (*z + w = w + z*)
1.19 - \<^rule_thm>\<open>add.left_commute\<close>,
1.20 - (*x + (y + z) = y + (x + z)*)
1.21 - \<^rule_thm>\<open>add.assoc\<close>
1.22 - (*z1.0 + z2.0 + z3.0 = z1.0 + (z2.0 + z3.0)*)
1.23 - ],
1.24 - scr = Rule.Empty_Prog};
1.25 + Rule_Def.Repeat{
1.26 + id = "order_add_mult_System", preconds = [],
1.27 + rew_ord = ("ord_simplify_System", ord_simplify_System false @{theory "Integrate"}),
1.28 + erls = Rule_Set.empty,srls = Rule_Set.Empty, calc = [], errpatts = [],
1.29 + rules = [
1.30 + \<^rule_thm>\<open>mult.commute\<close>, (* z * w = w * z *)
1.31 + \<^rule_thm>\<open>real_mult_left_commute\<close>, (*z1.0 * (z2.0 * z3.0) = z2.0 * (z1.0 * z3.0)*)
1.32 + \<^rule_thm>\<open>mult.assoc\<close>, (*z1.0 * z2.0 * z3.0 = z1.0 * (z2.0 * z3.0)*)
1.33 + \<^rule_thm>\<open>add.commute\<close>, (*z + w = w + z*)
1.34 + \<^rule_thm>\<open>add.left_commute\<close>, (*x + (y + z) = y + (x + z)*)
1.35 + \<^rule_thm>\<open>add.assoc\<close> ], (*z1.0 + z2.0 + z3.0 = z1.0 + (z2.0 + z3.0)*)
1.36 + scr = Rule.Empty_Prog};
1.37 \<close>
1.38 ML \<open>
1.39 (*.adapted from 'norm_Rational' by
1.40 @@ -194,42 +188,38 @@
1.41 #2 NOT using common_nominator_p .*)
1.42 val norm_System_noadd_fractions =
1.43 Rule_Def.Repeat {id = "norm_System_noadd_fractions", preconds = [],
1.44 - rew_ord = ("dummy_ord",Rewrite_Ord.dummy_ord),
1.45 - erls = norm_rat_erls, srls = Rule_Set.Empty, calc = [], errpatts = [],
1.46 - rules = [(*sequence given by operator precedence*)
1.47 - Rule.Rls_ discard_minus,
1.48 - Rule.Rls_ powers,
1.49 - Rule.Rls_ rat_mult_divide,
1.50 - Rule.Rls_ expand,
1.51 - Rule.Rls_ reduce_0_1_2,
1.52 - Rule.Rls_ (*order_add_mult #1*) order_add_mult_System,
1.53 - Rule.Rls_ collect_numerals,
1.54 - (*Rule.Rls_ add_fractions_p, #2*)
1.55 - Rule.Rls_ cancel_p
1.56 - ],
1.57 - scr = Rule.Empty_Prog
1.58 - };
1.59 + rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord),
1.60 + erls = norm_rat_erls, srls = Rule_Set.Empty, calc = [], errpatts = [],
1.61 + rules = [(*sequence given by operator precedence*)
1.62 + Rule.Rls_ discard_minus,
1.63 + Rule.Rls_ powers,
1.64 + Rule.Rls_ rat_mult_divide,
1.65 + Rule.Rls_ expand,
1.66 + Rule.Rls_ reduce_0_1_2,
1.67 + Rule.Rls_ (*order_add_mult #1*) order_add_mult_System,
1.68 + Rule.Rls_ collect_numerals,
1.69 + (*Rule.Rls_ add_fractions_p, #2*)
1.70 + Rule.Rls_ cancel_p],
1.71 + scr = Rule.Empty_Prog};
1.72 \<close>
1.73 ML \<open>
1.74 (*.adapted from 'norm_Rational' by
1.75 *1* using 'ord_simplify_System' in 'order_add_mult_System'.*)
1.76 val norm_System =
1.77 Rule_Def.Repeat {id = "norm_System", preconds = [],
1.78 - rew_ord = ("dummy_ord",Rewrite_Ord.dummy_ord),
1.79 - erls = norm_rat_erls, srls = Rule_Set.Empty, calc = [], errpatts = [],
1.80 - rules = [(*sequence given by operator precedence*)
1.81 - Rule.Rls_ discard_minus,
1.82 - Rule.Rls_ powers,
1.83 - Rule.Rls_ rat_mult_divide,
1.84 - Rule.Rls_ expand,
1.85 - Rule.Rls_ reduce_0_1_2,
1.86 - Rule.Rls_ (*order_add_mult *1*) order_add_mult_System,
1.87 - Rule.Rls_ collect_numerals,
1.88 - Rule.Rls_ add_fractions_p,
1.89 - Rule.Rls_ cancel_p
1.90 - ],
1.91 - scr = Rule.Empty_Prog
1.92 - };
1.93 + rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord),
1.94 + erls = norm_rat_erls, srls = Rule_Set.Empty, calc = [], errpatts = [],
1.95 + rules = [(*sequence given by operator precedence*)
1.96 + Rule.Rls_ discard_minus,
1.97 + Rule.Rls_ powers,
1.98 + Rule.Rls_ rat_mult_divide,
1.99 + Rule.Rls_ expand,
1.100 + Rule.Rls_ reduce_0_1_2,
1.101 + Rule.Rls_ (*order_add_mult *1*) order_add_mult_System,
1.102 + Rule.Rls_ collect_numerals,
1.103 + Rule.Rls_ add_fractions_p,
1.104 + Rule.Rls_ cancel_p],
1.105 + scr = Rule.Empty_Prog};
1.106 \<close>
1.107 ML \<open>
1.108 (*.simplify an equational system BEFORE solving it such that parentheses are
1.109 @@ -243,22 +233,18 @@
1.110 analoguous to simplify_Integral .*)
1.111 val simplify_System_parenthesized =
1.112 Rule_Set.Sequence {id = "simplify_System_parenthesized", preconds = []:term list,
1.113 - rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord),
1.114 - erls = Atools_erls, srls = Rule_Set.Empty, calc = [], errpatts = [],
1.115 - rules = [\<^rule_thm>\<open>distrib_right\<close>,
1.116 - (*"(?z1.0 + ?z2.0) * ?w = ?z1.0 * ?w + ?z2.0 * ?w"*)
1.117 - \<^rule_thm>\<open>add_divide_distrib\<close>,
1.118 - (*"(?x + ?y) / ?z = ?x / ?z + ?y / ?z"*)
1.119 - (*^^^^^ *0* ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^*)
1.120 - Rule.Rls_ norm_Rational_noadd_fractions(**2**),
1.121 - Rule.Rls_ (*order_add_mult_in*) norm_System_noadd_fractions (**1**),
1.122 - \<^rule_thm_sym>\<open>mult.assoc\<close>
1.123 - (*Rule.Rls_ discard_parentheses *3**),
1.124 - Rule.Rls_ collect_bdv, (*from make_polynomial_in WN051031 welldone?*)
1.125 - Rule.Rls_ separate_bdv2,
1.126 - \<^rule_eval>\<open>divide\<close> (Prog_Expr.eval_cancel "#divide_e")
1.127 - ],
1.128 - scr = Rule.Empty_Prog};
1.129 + rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord),
1.130 + erls = Atools_erls, srls = Rule_Set.Empty, calc = [], errpatts = [],
1.131 + rules = [
1.132 + \<^rule_thm>\<open>distrib_right\<close>, (*"(?z1.0 + ?z2.0) * ?w = ?z1.0 * ?w + ?z2.0 * ?w"*)
1.133 + \<^rule_thm>\<open>add_divide_distrib\<close>, (*"(?x + ?y) / ?z = ?x / ?z + ?y / ?z"*)
1.134 + Rule.Rls_ norm_Rational_noadd_fractions,
1.135 + Rule.Rls_ (*order_add_mult_in*) norm_System_noadd_fractions,
1.136 + \<^rule_thm_sym>\<open>mult.assoc\<close>,
1.137 + Rule.Rls_ collect_bdv, (*from make_polynomial_in WN051031 welldone?*)
1.138 + Rule.Rls_ separate_bdv2,
1.139 + \<^rule_eval>\<open>divide\<close> (Prog_Expr.eval_cancel "#divide_e")],
1.140 + scr = Rule.Empty_Prog};
1.141 \<close>
1.142 ML \<open>
1.143 (*.simplify an equational system AFTER solving it;
1.144 @@ -267,16 +253,16 @@
1.145 (*TODO.WN051031 ^^^^^^^^^^ should be in EACH rls contained *)
1.146 val simplify_System =
1.147 Rule_Set.Sequence {id = "simplify_System", preconds = []:term list,
1.148 - rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord),
1.149 - erls = Atools_erls, srls = Rule_Set.Empty, calc = [], errpatts = [],
1.150 - rules = [Rule.Rls_ norm_Rational,
1.151 - Rule.Rls_ (*order_add_mult_in*) norm_System (**1**),
1.152 - Rule.Rls_ discard_parentheses,
1.153 - Rule.Rls_ collect_bdv, (*from make_polynomial_in WN051031 welldone?*)
1.154 - Rule.Rls_ separate_bdv2,
1.155 - \<^rule_eval>\<open>divide\<close> (Prog_Expr.eval_cancel "#divide_e")
1.156 - ],
1.157 - scr = Rule.Empty_Prog};
1.158 + rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord),
1.159 + erls = Atools_erls, srls = Rule_Set.Empty, calc = [], errpatts = [],
1.160 + rules = [
1.161 + Rule.Rls_ norm_Rational,
1.162 + Rule.Rls_ (*order_add_mult_in*) norm_System (**1**),
1.163 + Rule.Rls_ discard_parentheses,
1.164 + Rule.Rls_ collect_bdv, (*from make_polynomial_in WN051031 welldone?*)
1.165 + Rule.Rls_ separate_bdv2,
1.166 + \<^rule_eval>\<open>divide\<close> (Prog_Expr.eval_cancel "#divide_e")],
1.167 + scr = Rule.Empty_Prog};
1.168 (*
1.169 val simplify_System =
1.170 Rule_Set.append_rules "simplify_System" simplify_System_parenthesized
1.171 @@ -285,36 +271,35 @@
1.172 \<close>
1.173 ML \<open>
1.174 val isolate_bdvs =
1.175 - Rule_Def.Repeat {id="isolate_bdvs", preconds = [],
1.176 - rew_ord = ("e_rew_ord", Rewrite_Ord.e_rew_ord),
1.177 - erls = Rule_Set.append_rules "erls_isolate_bdvs" Rule_Set.empty
1.178 - [(\<^rule_eval>\<open>occur_exactly_in\<close> (eval_occur_exactly_in "#eval_occur_exactly_in_"))],
1.179 - srls = Rule_Set.Empty, calc = [], errpatts = [],
1.180 - rules =
1.181 - [\<^rule_thm>\<open>commute_0_equality\<close>,
1.182 - \<^rule_thm>\<open>separate_bdvs_add\<close>,
1.183 - \<^rule_thm>\<open>separate_bdvs_mult\<close>],
1.184 - scr = Rule.Empty_Prog};
1.185 + Rule_Def.Repeat {
1.186 + id="isolate_bdvs", preconds = [], rew_ord = ("e_rew_ord", Rewrite_Ord.e_rew_ord),
1.187 + erls = Rule_Set.append_rules "erls_isolate_bdvs" Rule_Set.empty [
1.188 + (\<^rule_eval>\<open>occur_exactly_in\<close> (eval_occur_exactly_in "#eval_occur_exactly_in_"))],
1.189 + srls = Rule_Set.Empty, calc = [], errpatts = [],
1.190 + rules = [
1.191 + \<^rule_thm>\<open>commute_0_equality\<close>,
1.192 + \<^rule_thm>\<open>separate_bdvs_add\<close>,
1.193 + \<^rule_thm>\<open>separate_bdvs_mult\<close>],
1.194 + scr = Rule.Empty_Prog};
1.195 \<close>
1.196 ML \<open>
1.197 val isolate_bdvs_4x4 =
1.198 - Rule_Def.Repeat {id="isolate_bdvs_4x4", preconds = [],
1.199 - rew_ord = ("e_rew_ord", Rewrite_Ord.e_rew_ord),
1.200 - erls = Rule_Set.append_rules
1.201 - "erls_isolate_bdvs_4x4" Rule_Set.empty
1.202 - [\<^rule_eval>\<open>occur_exactly_in\<close> (eval_occur_exactly_in "#eval_occur_exactly_in_"),
1.203 - \<^rule_eval>\<open>Prog_Expr.ident\<close> (Prog_Expr.eval_ident "#ident_"),
1.204 - \<^rule_eval>\<open>Prog_Expr.some_occur_in\<close> (Prog_Expr.eval_some_occur_in "#some_occur_in_"),
1.205 - \<^rule_thm>\<open>not_true\<close>,
1.206 - \<^rule_thm>\<open>not_false\<close>
1.207 - ],
1.208 - srls = Rule_Set.Empty, calc = [], errpatts = [],
1.209 - rules = [\<^rule_thm>\<open>commute_0_equality\<close>,
1.210 - \<^rule_thm>\<open>separate_bdvs0\<close>,
1.211 - \<^rule_thm>\<open>separate_bdvs_add1\<close>,
1.212 - \<^rule_thm>\<open>separate_bdvs_add2\<close>,
1.213 - \<^rule_thm>\<open>separate_bdvs_mult\<close>
1.214 - ], scr = Rule.Empty_Prog};
1.215 + Rule_Def.Repeat {id="isolate_bdvs_4x4", preconds = [],
1.216 + rew_ord = ("e_rew_ord", Rewrite_Ord.e_rew_ord),
1.217 + erls = Rule_Set.append_rules "erls_isolate_bdvs_4x4" Rule_Set.empty [
1.218 + \<^rule_eval>\<open>occur_exactly_in\<close> (eval_occur_exactly_in "#eval_occur_exactly_in_"),
1.219 + \<^rule_eval>\<open>Prog_Expr.ident\<close> (Prog_Expr.eval_ident "#ident_"),
1.220 + \<^rule_eval>\<open>Prog_Expr.some_occur_in\<close> (Prog_Expr.eval_some_occur_in "#some_occur_in_"),
1.221 + \<^rule_thm>\<open>not_true\<close>,
1.222 + \<^rule_thm>\<open>not_false\<close>],
1.223 + srls = Rule_Set.Empty, calc = [], errpatts = [],
1.224 + rules = [
1.225 + \<^rule_thm>\<open>commute_0_equality\<close>,
1.226 + \<^rule_thm>\<open>separate_bdvs0\<close>,
1.227 + \<^rule_thm>\<open>separate_bdvs_add1\<close>,
1.228 + \<^rule_thm>\<open>separate_bdvs_add2\<close>,
1.229 + \<^rule_thm>\<open>separate_bdvs_mult\<close>],
1.230 + scr = Rule.Empty_Prog};
1.231
1.232 \<close>
1.233 ML \<open>
1.234 @@ -322,65 +307,59 @@
1.235 (*.order the equations in a system such, that a triangular system (if any)
1.236 appears as [..c_4 = .., ..., ..., ..c_1 + ..c_2 + ..c_3 ..c_4 = ..].*)
1.237 val order_system =
1.238 - Rule_Def.Repeat {id="order_system", preconds = [],
1.239 - rew_ord = ("ord_simplify_System",
1.240 - ord_simplify_System false \<^theory>),
1.241 - erls = Rule_Set.Empty, srls = Rule_Set.Empty, calc = [], errpatts = [],
1.242 - rules = [\<^rule_thm>\<open>order_system_NxN\<close>
1.243 - ],
1.244 - scr = Rule.Empty_Prog};
1.245 + Rule_Def.Repeat {id="order_system", preconds = [],
1.246 + rew_ord = ("ord_simplify_System", ord_simplify_System false \<^theory>),
1.247 + erls = Rule_Set.Empty, srls = Rule_Set.Empty, calc = [], errpatts = [],
1.248 + rules = [
1.249 + \<^rule_thm>\<open>order_system_NxN\<close>],
1.250 + scr = Rule.Empty_Prog};
1.251
1.252 val prls_triangular =
1.253 - Rule_Def.Repeat {id="prls_triangular", preconds = [],
1.254 - rew_ord = ("e_rew_ord", Rewrite_Ord.e_rew_ord),
1.255 - erls = Rule_Def.Repeat {id="erls_prls_triangular", preconds = [],
1.256 - rew_ord = ("e_rew_ord", Rewrite_Ord.e_rew_ord),
1.257 - erls = Rule_Set.Empty, srls = Rule_Set.Empty, calc = [], errpatts = [],
1.258 - rules = [(*for precond NTH_CONS ...*)
1.259 - \<^rule_eval>\<open>less\<close> (Prog_Expr.eval_equ "#less_"),
1.260 - \<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_"),
1.261 - Rule.Eval ("EqSystem.occur_exactly_in",
1.262 - eval_occur_exactly_in "#eval_occur_exactly_in_")
1.263 - (*immediately repeated rewrite pushes
1.264 - '+' into precondition !*)
1.265 - ],
1.266 - scr = Rule.Empty_Prog},
1.267 - srls = Rule_Set.Empty, calc = [], errpatts = [],
1.268 - rules = [\<^rule_thm>\<open>NTH_CONS\<close>,
1.269 - \<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_"),
1.270 - \<^rule_thm>\<open>NTH_NIL\<close>,
1.271 - \<^rule_thm>\<open>tl_Cons\<close>,
1.272 - \<^rule_thm>\<open>tl_Nil\<close>,
1.273 - \<^rule_eval>\<open>occur_exactly_in\<close> (eval_occur_exactly_in "#eval_occur_exactly_in_")
1.274 - ],
1.275 - scr = Rule.Empty_Prog};
1.276 + Rule_Def.Repeat {
1.277 + id="prls_triangular", preconds = [], rew_ord = ("e_rew_ord", Rewrite_Ord.e_rew_ord),
1.278 + erls = Rule_Def.Repeat {
1.279 + id="erls_prls_triangular", preconds = [], rew_ord = ("e_rew_ord", Rewrite_Ord.e_rew_ord),
1.280 + erls = Rule_Set.Empty, srls = Rule_Set.Empty, calc = [], errpatts = [],
1.281 + rules = [(*for precond NTH_CONS ...*)
1.282 + \<^rule_eval>\<open>less\<close> (Prog_Expr.eval_equ "#less_"),
1.283 + \<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_"),
1.284 + \<^rule_eval>\<open>occur_exactly_in\<close> (eval_occur_exactly_in "#eval_occur_exactly_in_")],
1.285 + (*immediately repeated rewrite pushes '+' into precondition !*)
1.286 + scr = Rule.Empty_Prog},
1.287 + srls = Rule_Set.Empty, calc = [], errpatts = [],
1.288 + rules = [
1.289 + \<^rule_thm>\<open>NTH_CONS\<close>,
1.290 + \<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_"),
1.291 + \<^rule_thm>\<open>NTH_NIL\<close>,
1.292 + \<^rule_thm>\<open>tl_Cons\<close>,
1.293 + \<^rule_thm>\<open>tl_Nil\<close>,
1.294 + \<^rule_eval>\<open>occur_exactly_in\<close> (eval_occur_exactly_in "#eval_occur_exactly_in_")],
1.295 + scr = Rule.Empty_Prog};
1.296 \<close>
1.297 ML \<open>
1.298
1.299 (*WN060914 quickly created for 4x4;
1.300 more similarity to prls_triangular desirable*)
1.301 val prls_triangular4 =
1.302 - Rule_Def.Repeat {id="prls_triangular4", preconds = [],
1.303 - rew_ord = ("e_rew_ord", Rewrite_Ord.e_rew_ord),
1.304 - erls = Rule_Def.Repeat {id="erls_prls_triangular4", preconds = [],
1.305 - rew_ord = ("e_rew_ord", Rewrite_Ord.e_rew_ord),
1.306 - erls = Rule_Set.Empty, srls = Rule_Set.Empty, calc = [], errpatts = [],
1.307 - rules = [(*for precond NTH_CONS ...*)
1.308 - \<^rule_eval>\<open>less\<close> (Prog_Expr.eval_equ "#less_"),
1.309 - \<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_")
1.310 - (*immediately repeated rewrite pushes
1.311 - '+' into precondition !*)
1.312 - ],
1.313 - scr = Rule.Empty_Prog},
1.314 - srls = Rule_Set.Empty, calc = [], errpatts = [],
1.315 - rules = [\<^rule_thm>\<open>NTH_CONS\<close>,
1.316 - \<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_"),
1.317 - \<^rule_thm>\<open>NTH_NIL\<close>,
1.318 - \<^rule_thm>\<open>tl_Cons\<close>,
1.319 - \<^rule_thm>\<open>tl_Nil\<close>,
1.320 - \<^rule_eval>\<open>occur_exactly_in\<close> (eval_occur_exactly_in "#eval_occur_exactly_in_")
1.321 - ],
1.322 - scr = Rule.Empty_Prog};
1.323 + Rule_Def.Repeat {
1.324 + id="prls_triangular4", preconds = [], rew_ord = ("e_rew_ord", Rewrite_Ord.e_rew_ord),
1.325 + erls = Rule_Def.Repeat {
1.326 + id="erls_prls_triangular4", preconds = [], rew_ord = ("e_rew_ord", Rewrite_Ord.e_rew_ord),
1.327 + erls = Rule_Set.Empty, srls = Rule_Set.Empty, calc = [], errpatts = [],
1.328 + rules = [(*for precond NTH_CONS ...*)
1.329 + \<^rule_eval>\<open>less\<close> (Prog_Expr.eval_equ "#less_"),
1.330 + \<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_")],
1.331 + (*immediately repeated rewrite pushes '+' into precondition !*)
1.332 + scr = Rule.Empty_Prog},
1.333 + srls = Rule_Set.Empty, calc = [], errpatts = [],
1.334 + rules = [
1.335 + \<^rule_thm>\<open>NTH_CONS\<close>,
1.336 + \<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_"),
1.337 + \<^rule_thm>\<open>NTH_NIL\<close>,
1.338 + \<^rule_thm>\<open>tl_Cons\<close>,
1.339 + \<^rule_thm>\<open>tl_Nil\<close>,
1.340 + \<^rule_eval>\<open>occur_exactly_in\<close> (eval_occur_exactly_in "#eval_occur_exactly_in_")],
1.341 + scr = Rule.Empty_Prog};
1.342 \<close>
1.343
1.344 rule_set_knowledge
1.345 @@ -624,7 +603,7 @@
1.346 \<open>{rew_ord'="ord_simplify_System", rls' = Rule_Set.Empty, calc = [],
1.347 srls = Rule_Set.append_rules "srls_top_down_4x4" srls [],
1.348 prls = Rule_Set.append_rules "prls_tri_4x4_lin_sys" prls_triangular
1.349 - [\<^rule_eval>\<open>Prog_Expr.occurs_in\<close> (Prog_Expr.eval_occurs_in "")],
1.350 + [\<^rule_eval>\<open>Prog_Expr.occurs_in\<close> (Prog_Expr.eval_occurs_in "")],
1.351 crls = Rule_Set.Empty, errpats = [], nrls = Rule_Set.Empty}\<close>
1.352 (*FIXXXXME.WN060916: this script works ONLY for exp 7.79 #>#>#>#>#>#>#>#>#>#>*)
1.353 Program: solve_system4.simps