811 \<open>{rew_ord="Rewrite_Ord.id_empty",rls'=tval_rls, |
811 \<open>{rew_ord="Rewrite_Ord.id_empty",rls'=tval_rls, |
812 prog_rls = Rule_Set.append_rules "srls_contains_root" Rule_Set.empty |
812 prog_rls = Rule_Set.append_rules "srls_contains_root" Rule_Set.empty |
813 [\<^rule_eval>\<open>contains_root\<close> (eval_contains_root "")], |
813 [\<^rule_eval>\<open>contains_root\<close> (eval_contains_root "")], |
814 where_rls = Rule_Set.append_rules "prls_contains_root" Rule_Set.empty |
814 where_rls = Rule_Set.append_rules "prls_contains_root" Rule_Set.empty |
815 [\<^rule_eval>\<open>contains_root\<close> (eval_contains_root "")], |
815 [\<^rule_eval>\<open>contains_root\<close> (eval_contains_root "")], |
816 calc=[],errpats = [], rew_rls = Rule_Set.empty (*,asm_rls=[], |
816 calc = [], errpats = [], rew_rls = Rule_Set.empty}\<close> |
817 asm_thm=[("square_equation_left", ""), ("square_equation_right", "")]*)}\<close> |
|
818 Program: solve_root_equ.simps |
817 Program: solve_root_equ.simps |
819 Given: "equality e_e" "solveFor v_v" |
818 Given: "equality e_e" "solveFor v_v" |
820 Where: "contains_root (e_e::bool)" |
819 Where: "contains_root (e_e::bool)" |
821 Find: "solutions v_v'i'" |
820 Find: "solutions v_v'i'" |
822 |
821 |