equal
deleted
inserted
replaced
86 ML \<open> |
86 ML \<open> |
87 |
87 |
88 (*isolate the bound variable in an linear equation; 'bdv' is a meta-constant*) |
88 (*isolate the bound variable in an linear equation; 'bdv' is a meta-constant*) |
89 val LinEq_simplify = prep_rls'( |
89 val LinEq_simplify = prep_rls'( |
90 Rule_Def.Repeat {id = "LinEq_simplify", preconds = [], |
90 Rule_Def.Repeat {id = "LinEq_simplify", preconds = [], |
91 rew_ord = ("e_rew_ord", Rewrite_Ord.e_rew_ord), |
91 rew_ord = ("Rewrite_Ord.id_empty", Rewrite_Ord.function_empty), |
92 erls = LinEq_erls, |
92 erls = LinEq_erls, |
93 srls = Rule_Set.Empty, |
93 srls = Rule_Set.Empty, |
94 calc = [], errpatts = [], |
94 calc = [], errpatts = [], |
95 rules = [ |
95 rules = [ |
96 \<^rule_thm>\<open>lin_isolate_add1\<close>, (* a+bx=0 -> bx=-a *) |
96 \<^rule_thm>\<open>lin_isolate_add1\<close>, (* a+bx=0 -> bx=-a *) |