Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Theorem "_" is now stored with open derivation.
authorberghofe
Fri, 31 Oct 2008 10:39:04 +0100
changeset 28713 135317cd34d6
parent 28712 4f2954d995f0
child 28714 1992553cccfe
Theorem "_" is now stored with open derivation.
src/Pure/drule.ML file | annotate | diff | comparison | revisions 
--- a/src/Pure/drule.ML	Fri Oct 31 10:37:34 2008 +0100
+++ b/src/Pure/drule.ML	Fri Oct 31 10:39:04 2008 +0100
@@ -584,7 +584,7 @@
 
 (*The rule V/V, obtains assumption solving for eresolve_tac*)
 val asm_rl = store_standard_thm_open "asm_rl" (Thm.trivial (read_prop "?psi"));
-val _ = store_thm "_" asm_rl;
+val _ = store_thm_open "_" asm_rl;
 
 (*Meta-level cut rule: [| V==>W; V |] ==> W *)
 val cut_rl =
isabelle