equal
deleted
inserted
replaced
532 \<^rule_thm>\<open>rroot_to_lhs_mult\<close>, |
532 \<^rule_thm>\<open>rroot_to_lhs_mult\<close>, |
533 \<^rule_thm>\<open>rroot_to_lhs_add_mult\<close>, |
533 \<^rule_thm>\<open>rroot_to_lhs_add_mult\<close>, |
534 \<^rule_thm>\<open>risolate_root_add\<close>, |
534 \<^rule_thm>\<open>risolate_root_add\<close>, |
535 \<^rule_thm>\<open>risolate_root_mult\<close>, |
535 \<^rule_thm>\<open>risolate_root_mult\<close>, |
536 \<^rule_thm>\<open>risolate_root_div\<close> ], |
536 \<^rule_thm>\<open>risolate_root_div\<close> ], |
537 scr = Rule.Prog ((Thm.term_of o the o (TermC.parse \<^theory>)) |
537 scr = Rule.Prog (TermC.parseNEW'' \<^theory> "empty_script") |
538 "empty_script") |
|
539 }; |
538 }; |
540 |
539 |
541 (*isolate the bound variable in an equation; 'bdv' is a meta-constant*) |
540 (*isolate the bound variable in an equation; 'bdv' is a meta-constant*) |
542 val isolate_bdv = |
541 val isolate_bdv = |
543 Rule_Def.Repeat{id = "isolate_bdv", preconds = [], rew_ord = ("e_rew_ord",Rewrite_Ord.e_rew_ord), |
542 Rule_Def.Repeat{id = "isolate_bdv", preconds = [], rew_ord = ("e_rew_ord",Rewrite_Ord.e_rew_ord), |
548 \<^rule_thm>\<open>risolate_bdv_mult\<close>, |
547 \<^rule_thm>\<open>risolate_bdv_mult\<close>, |
549 \<^rule_thm>\<open>mult_square\<close>, |
548 \<^rule_thm>\<open>mult_square\<close>, |
550 \<^rule_thm>\<open>constant_square\<close>, |
549 \<^rule_thm>\<open>constant_square\<close>, |
551 \<^rule_thm>\<open>constant_mult_square\<close> |
550 \<^rule_thm>\<open>constant_mult_square\<close> |
552 ], |
551 ], |
553 scr = Rule.Prog ((Thm.term_of o the o (TermC.parse \<^theory>)) |
552 scr = Rule.Prog (TermC.parseNEW'' \<^theory> "empty_script") |
554 "empty_script") |
|
555 }; |
553 }; |
556 \<close> |
554 \<close> |
557 ML \<open>val prep_rls' = Auto_Prog.prep_rls @{theory};\<close> |
555 ML \<open>val prep_rls' = Auto_Prog.prep_rls @{theory};\<close> |
558 rule_set_knowledge |
556 rule_set_knowledge |
559 Test_simplify = \<open>prep_rls' Test_simplify\<close> and |
557 Test_simplify = \<open>prep_rls' Test_simplify\<close> and |