changeset 42471 | 593289343c7d |
parent 40722 | 441260986b63 |
child 43324 | 2b47822868e4 |
--- a/src/Pure/drule.ML Sat Apr 23 19:22:11 2011 +0200 +++ b/src/Pure/drule.ML Sat Apr 23 19:41:53 2011 +0200 @@ -565,7 +565,6 @@ (*The rule V/V, obtains assumption solving for eresolve_tac*) val asm_rl = store_standard_thm_open (Binding.name "asm_rl") (Thm.trivial (read_prop "?psi")); -val _ = store_thm_open (Binding.name "_") asm_rl; (*Meta-level cut rule: [| V==>W; V |] ==> W *) val cut_rl =