# HG changeset patch
# User wenzelm
# Date 935773167 -7200
# Node ID 2bcee6a460d8ddcef4df9208a251d068f18e7af4
# Parent  999b1b777fc238c1344fa9e7bceccfedc8722f91
thm "_" = asm_rl;

diff -r 999b1b777fc2 -r 2bcee6a460d8 src/Pure/drule.ML
--- a/src/Pure/drule.ML	Fri Aug 27 15:52:32 1999 +0200
+++ b/src/Pure/drule.ML	Fri Aug 27 18:59:27 1999 +0200
@@ -535,8 +535,8 @@
 (*** Some useful meta-theorems ***)
 
 (*The rule V/V, obtains assumption solving for eresolve_tac*)
-val asm_rl =
-  store_thm "asm_rl" (trivial(read_prop "PROP ?psi"));
+val asm_rl = store_thm "asm_rl" (trivial(read_prop "PROP ?psi"));
+val _ = store_thm "_" asm_rl;
 
 (*Meta-level cut rule: [| V==>W; V |] ==> W *)
 val cut_rl =