--- a/src/FOL/IFOL.thy Fri Oct 24 10:41:15 2008 +0200
+++ b/src/FOL/IFOL.thy Fri Oct 24 17:48:33 2008 +0200
@@ -101,6 +101,7 @@
(* Equality *)
refl: "a=a"
+ subst: "a=b \<Longrightarrow> P(a) \<Longrightarrow> P(b)"
(* Propositional logic *)
@@ -125,7 +126,10 @@
exI: "P(x) ==> (EX x. P(x))"
exE: "[| EX x. P(x); !!x. P(x) ==> R |] ==> R"
- (* Reflection *)
+
+axioms
+
+ (* Reflection, admissible *)
eq_reflection: "(x=y) ==> (x==y)"
iff_reflection: "(P<->Q) ==> (P==Q)"
@@ -134,18 +138,6 @@
lemmas strip = impI allI
-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 *)