--- a/src/FOL/IFOL.thy Thu Jun 18 09:07:54 2020 +0000
+++ b/src/FOL/IFOL.thy Fri Jun 19 09:46:47 2020 +0000
@@ -829,32 +829,34 @@
lemma subst_all:
\<open>(\<And>x. x = a \<Longrightarrow> PROP P(x)) \<equiv> PROP P(a)\<close>
-proof (rule equal_intr_rule)
- assume *: \<open>\<And>x. x = a \<Longrightarrow> PROP P(x)\<close>
- show \<open>PROP P(a)\<close>
- by (rule *) (rule refl)
-next
- fix x
- assume \<open>PROP P(a)\<close> and \<open>x = a\<close>
- from \<open>x = a\<close> have \<open>x \<equiv> a\<close>
- by (rule eq_reflection)
- with \<open>PROP P(a)\<close> show \<open>PROP P(x)\<close>
- by simp
-qed
-
-lemma subst_all':
\<open>(\<And>x. a = x \<Longrightarrow> PROP P(x)) \<equiv> PROP P(a)\<close>
-proof (rule equal_intr_rule)
- assume *: \<open>\<And>x. a = x \<Longrightarrow> PROP P(x)\<close>
- show \<open>PROP P(a)\<close>
- by (rule *) (rule refl)
-next
- fix x
- assume \<open>PROP P(a)\<close> and \<open>a = x\<close>
- from \<open>a = x\<close> have \<open>a \<equiv> x\<close>
- by (rule eq_reflection)
- with \<open>PROP P(a)\<close> show \<open>PROP P(x)\<close>
- by simp
+proof -
+ show \<open>(\<And>x. x = a \<Longrightarrow> PROP P(x)) \<equiv> PROP P(a)\<close>
+ proof (rule equal_intr_rule)
+ assume *: \<open>\<And>x. x = a \<Longrightarrow> PROP P(x)\<close>
+ show \<open>PROP P(a)\<close>
+ by (rule *) (rule refl)
+ next
+ fix x
+ assume \<open>PROP P(a)\<close> and \<open>x = a\<close>
+ from \<open>x = a\<close> have \<open>x \<equiv> a\<close>
+ by (rule eq_reflection)
+ with \<open>PROP P(a)\<close> show \<open>PROP P(x)\<close>
+ by simp
+ qed
+ show \<open>(\<And>x. a = x \<Longrightarrow> PROP P(x)) \<equiv> PROP P(a)\<close>
+ proof (rule equal_intr_rule)
+ assume *: \<open>\<And>x. a = x \<Longrightarrow> PROP P(x)\<close>
+ show \<open>PROP P(a)\<close>
+ by (rule *) (rule refl)
+ next
+ fix x
+ assume \<open>PROP P(a)\<close> and \<open>a = x\<close>
+ from \<open>a = x\<close> have \<open>a \<equiv> x\<close>
+ by (rule eq_reflection)
+ with \<open>PROP P(a)\<close> show \<open>PROP P(x)\<close>
+ by simp
+ qed
qed