equal
deleted
inserted
replaced
437 Rule_Def.Repeat {id = "d0_polyeq_simplify", preconds = [], |
437 Rule_Def.Repeat {id = "d0_polyeq_simplify", preconds = [], |
438 rew_ord = ("e_rew_ord",Rewrite_Ord.e_rew_ord), |
438 rew_ord = ("e_rew_ord",Rewrite_Ord.e_rew_ord), |
439 erls = PolyEq_erls, |
439 erls = PolyEq_erls, |
440 srls = Rule_Set.Empty, |
440 srls = Rule_Set.Empty, |
441 calc = [], errpatts = [], |
441 calc = [], errpatts = [], |
442 rules = [\<^rule_thm>\<open>d0_true\<close>, |
442 rules = [\<^rule_thm>\<open>d0_true\<close>, \<^rule_thm>\<open>d0_false\<close>], |
443 Rule.Thm("d0_false",ThmC.numerals_to_Free @{thm d0_false}) |
|
444 ], |
|
445 scr = Rule.Empty_Prog |
443 scr = Rule.Empty_Prog |
446 }); |
444 }); |
447 |
445 |
448 (* -- d1 -- *) |
446 (* -- d1 -- *) |
449 (*isolate the bound variable in an d1 equation; 'bdv' is a meta-constant*) |
447 (*isolate the bound variable in an d1 equation; 'bdv' is a meta-constant*) |
1303 \<^rule_thm>\<open>separate_bdv_n\<close>, |
1301 \<^rule_thm>\<open>separate_bdv_n\<close>, |
1304 \<^rule_thm>\<open>separate_1_bdv\<close>, |
1302 \<^rule_thm>\<open>separate_1_bdv\<close>, |
1305 (*"?bdv / ?b = (1 / ?b) * ?bdv"*) |
1303 (*"?bdv / ?b = (1 / ?b) * ?bdv"*) |
1306 \<^rule_thm>\<open>separate_1_bdv_n\<close>, |
1304 \<^rule_thm>\<open>separate_1_bdv_n\<close>, |
1307 (*"?bdv \<up> ?n / ?b = 1 / ?b * ?bdv \<up> ?n"*) |
1305 (*"?bdv \<up> ?n / ?b = 1 / ?b * ?bdv \<up> ?n"*) |
1308 Rule.Thm ("add_divide_distrib", |
1306 \<^rule_thm>\<open>add_divide_distrib\<close> |
1309 ThmC.numerals_to_Free @{thm add_divide_distrib}) |
|
1310 (*"(?x + ?y) / ?z = ?x / ?z + ?y / ?z" |
1307 (*"(?x + ?y) / ?z = ?x / ?z + ?y / ?z" |
1311 WN051031 DOES NOT BELONG TO HERE*) |
1308 WN051031 DOES NOT BELONG TO HERE*) |
1312 ]; |
1309 ]; |
1313 \<close> |
1310 \<close> |
1314 ML\<open> |
1311 ML\<open> |