# HG changeset patch
# User paulson
# Date 1102415474 -3600
# Node ID 3d99eea28a9bee062c9c74ddeba93497be9b6897
# Parent  302ef111b621030e8c7c6419428365d2b0397e10
proof of subst by S Merz

diff -r 302ef111b621 -r 3d99eea28a9b src/FOL/IFOL.thy
--- a/src/FOL/IFOL.thy	Mon Dec 06 14:14:03 2004 +0100
+++ b/src/FOL/IFOL.thy	Tue Dec 07 11:31:14 2004 +0100
@@ -82,7 +82,6 @@
   (* Equality *)
 
   refl:         "a=a"
-  subst:        "[| a=b;  P(a) |] ==> P(b)"
 
   (* Propositional logic *)
 
@@ -113,6 +112,18 @@
   iff_reflection: "(P<->Q) ==> (P==Q)"
 
 
+text{*Thanks to Stephan Merz*}
+theorem subst:
+  assumes eq: "a = b" and p: "P(a)"
+  shows "P(b)"
+proof -
+  from eq have meta: "a \<equiv> b"
+    by (rule eq_reflection)
+  from p show ?thesis
+    by (unfold meta)
+qed
+
+
 defs
   (* Definitions *)