--- a/src/HOL/HOL.thy Thu Jun 18 09:07:54 2020 +0000
+++ b/src/HOL/HOL.thy Fri Jun 19 09:46:47 2020 +0000
@@ -943,32 +943,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
lemma simp_thms:
@@ -1403,7 +1405,6 @@
all_simps
simp_thms
subst_all
- subst_all'
lemmas [cong] = imp_cong simp_implies_cong
lemmas [split] = if_split