src/FOL/hypsubstdata.ML
changeset 27572 67cd6ed76446
parent 21539 c5cf9243ad62
child 39159 0dec18004e75
--- a/src/FOL/hypsubstdata.ML	Mon Jul 14 17:02:55 2008 +0200
+++ b/src/FOL/hypsubstdata.ML	Mon Jul 14 17:47:18 2008 +0200
@@ -13,6 +13,8 @@
   val subst = thm "subst"
   val sym = thm "sym"
   val thin_refl = thm "thin_refl"
+  val prop_subst = @{lemma "PROP P(t) ==> PROP prop (x = t ==> PROP P(x))"
+                     by (unfold prop_def) (drule eq_reflection, unfold)}
 end;
 
 structure Hypsubst = HypsubstFun(Hypsubst_Data);