equal
deleted
inserted
replaced
153 tu: the terms to compare (t1, t2) ... *) |
153 tu: the terms to compare (t1, t2) ... *) |
154 fun sqrt_right (pr:bool) thy (_: Rule.subst) tu = |
154 fun sqrt_right (pr:bool) thy (_: Rule.subst) tu = |
155 (term_ord' pr thy(***) tu = LESS ); |
155 (term_ord' pr thy(***) tu = LESS ); |
156 end; |
156 end; |
157 |
157 |
158 Rule.rew_ord' := overwritel (! Rule.rew_ord', |
158 Rewrite_Ord.rew_ord' := overwritel (! Rewrite_Ord.rew_ord', |
159 [("termlessI", termlessI), |
159 [("termlessI", termlessI), |
160 ("sqrt_right", sqrt_right false @{theory "Pure"}) |
160 ("sqrt_right", sqrt_right false @{theory "Pure"}) |
161 ]); |
161 ]); |
162 |
162 |
163 (*-------------------------rulse-------------------------*) |
163 (*-------------------------rulse-------------------------*) |