src/FOLP/ROOT.ML
changeset 4223 f60e3d2c81d3
parent 4024 3c056eab237c
child 6349 f7750d816c21
--- a/src/FOLP/ROOT.ML	Wed Nov 12 16:28:53 1997 +0100
+++ b/src/FOLP/ROOT.ML	Wed Nov 12 18:58:50 1997 +0100
@@ -39,6 +39,8 @@
   val rev_mp = rev_mp
   val subst = subst
   val sym = sym
+  val thin_refl = prove_goal IFOLP.thy 
+		  "!!X. [|p:x=x; PROP W|] ==> PROP W" (K [atac 1]);
   end;
 
 structure Hypsubst = HypsubstFun(Hypsubst_Data);