equal
deleted
inserted
replaced
189 [("Root_erls",Root_erls) (*FIXXXME:del with rls.rls'*) |
189 [("Root_erls",Root_erls) (*FIXXXME:del with rls.rls'*) |
190 ]); |
190 ]); |
191 |
191 |
192 val make_rooteq = prep_rls( |
192 val make_rooteq = prep_rls( |
193 Rls{id = "make_rooteq", preconds = []:term list, |
193 Rls{id = "make_rooteq", preconds = []:term list, |
194 rew_ord = ("sqrt_right", sqrt_right false Root.thy), |
194 rew_ord = ("sqrt_right", sqrt_right false (theory "Root")), |
195 erls = Atools_erls, srls = Erls, |
195 erls = Atools_erls, srls = Erls, |
196 calc = [], |
196 calc = [], |
197 (*asm_thm = [],*) |
197 (*asm_thm = [],*) |
198 rules = [Thm ("real_diff_minus",num_str real_diff_minus), |
198 rules = [Thm ("real_diff_minus",num_str real_diff_minus), |
199 (*"a - b = a + (-1) * b"*) |
199 (*"a - b = a + (-1) * b"*) |