Theorem "_" is now stored with open derivation.
authorberghofe
Fri Oct 31 10:39:04 2008 +0100 (2008-10-31)
changeset 28713135317cd34d6
parent 28712 4f2954d995f0
child 28714 1992553cccfe
Theorem "_" is now stored with open derivation.
src/Pure/drule.ML
     1.1 --- a/src/Pure/drule.ML	Fri Oct 31 10:37:34 2008 +0100
     1.2 +++ b/src/Pure/drule.ML	Fri Oct 31 10:39:04 2008 +0100
     1.3 @@ -584,7 +584,7 @@
     1.4  
     1.5  (*The rule V/V, obtains assumption solving for eresolve_tac*)
     1.6  val asm_rl = store_standard_thm_open "asm_rl" (Thm.trivial (read_prop "?psi"));
     1.7 -val _ = store_thm "_" asm_rl;
     1.8 +val _ = store_thm_open "_" asm_rl;
     1.9  
    1.10  (*Meta-level cut rule: [| V==>W; V |] ==> W *)
    1.11  val cut_rl =