equal
deleted
inserted
replaced
207 | Const("HOL.one", _) => NONE |
207 | Const("HOL.one", _) => NONE |
208 | Const("Numeral.number_of", _) $ _ => NONE |
208 | Const("Numeral.number_of", _) $ _ => NONE |
209 | _ => SOME meta_UU_reorient; |
209 | _ => SOME meta_UU_reorient; |
210 in |
210 in |
211 val UU_reorient_simproc = |
211 val UU_reorient_simproc = |
212 Simplifier.simproc @{theory} "UU_reorient_simproc" ["UU=x"] reorient_proc |
212 Simplifier.simproc (the_context ()) "UU_reorient_simproc" ["UU=x"] reorient_proc |
213 end; |
213 end; |
214 |
214 |
215 Addsimprocs [UU_reorient_simproc]; |
215 Addsimprocs [UU_reorient_simproc]; |
216 *} |
216 *} |
217 |
217 |