# HG changeset patch
# User wenzelm
# Date 1464386304 -7200
# Node ID d4f459eb7ed044715abc2106885050acfda16193
# Parent  a0088f1c049d6285c2aab36ae413f653e48f80d3
tuned proofs;

diff -r a0088f1c049d -r d4f459eb7ed0 src/HOL/Complete_Lattices.thy
--- a/src/HOL/Complete_Lattices.thy	Fri May 27 23:35:13 2016 +0200
+++ b/src/HOL/Complete_Lattices.thy	Fri May 27 23:58:24 2016 +0200
@@ -484,11 +484,11 @@
 
 lemma sup_INF:
   "a \<squnion> (\<Sqinter>b\<in>B. f b) = (\<Sqinter>b\<in>B. a \<squnion> f b)"
-  unfolding sup_Inf by simp
+  by (simp add: sup_Inf)
 
 lemma inf_SUP:
   "a \<sqinter> (\<Squnion>b\<in>B. f b) = (\<Squnion>b\<in>B. a \<sqinter> f b)"
-  unfolding inf_Sup by simp
+  by (simp add: inf_Sup)
 
 lemma dual_complete_distrib_lattice:
   "class.complete_distrib_lattice Sup Inf sup (op \<ge>) (op >) inf \<top> \<bottom>"
@@ -607,19 +607,19 @@
 
 lemma Inf_less_iff:
   "\<Sqinter>S \<sqsubset> a \<longleftrightarrow> (\<exists>x\<in>S. x \<sqsubset> a)"
-  unfolding not_le [symmetric] le_Inf_iff by auto
+  by (simp add: not_le [symmetric] le_Inf_iff)
 
 lemma INF_less_iff:
   "(\<Sqinter>i\<in>A. f i) \<sqsubset> a \<longleftrightarrow> (\<exists>x\<in>A. f x \<sqsubset> a)"
-  using Inf_less_iff [of "f ` A"] by simp
+  by (simp add: Inf_less_iff [of "f ` A"])
 
 lemma less_Sup_iff:
   "a \<sqsubset> \<Squnion>S \<longleftrightarrow> (\<exists>x\<in>S. a \<sqsubset> x)"
-  unfolding not_le [symmetric] Sup_le_iff by auto
+  by (simp add: not_le [symmetric] Sup_le_iff)
 
 lemma less_SUP_iff:
   "a \<sqsubset> (\<Squnion>i\<in>A. f i) \<longleftrightarrow> (\<exists>x\<in>A. a \<sqsubset> f x)"
-  using less_Sup_iff [of _ "f ` A"] by simp
+  by (simp add: less_Sup_iff [of _ "f ` A"])
 
 lemma Sup_eq_top_iff [simp]:
   "\<Squnion>A = \<top> \<longleftrightarrow> (\<forall>x<\<top>. \<exists>i\<in>A. x < i)"
@@ -628,7 +628,7 @@
   show "(\<forall>x<\<top>. \<exists>i\<in>A. x < i)" unfolding * [symmetric]
   proof (intro allI impI)
     fix x assume "x < \<Squnion>A" then show "\<exists>i\<in>A. x < i"
-      unfolding less_Sup_iff by auto
+      by (simp add: less_Sup_iff)
   qed
 next
   assume *: "\<forall>x<\<top>. \<exists>i\<in>A. x < i"
diff -r a0088f1c049d -r d4f459eb7ed0 src/HOL/Orderings.thy
--- a/src/HOL/Orderings.thy	Fri May 27 23:35:13 2016 +0200
+++ b/src/HOL/Orderings.thy	Fri May 27 23:58:24 2016 +0200
@@ -134,7 +134,7 @@
 by (simp add: less_le_not_le)
 
 lemma less_imp_le: "x < y \<Longrightarrow> x \<le> y"
-unfolding less_le_not_le by blast
+by (simp add: less_le_not_le)
 
 
 text \<open>Asymmetry.\<close>
@@ -202,7 +202,7 @@
 by (fact order.order_iff_strict)
 
 lemma le_imp_less_or_eq: "x \<le> y \<Longrightarrow> x < y \<or> x = y"
-unfolding less_le by blast
+by (simp add: less_le)
 
 
 text \<open>Useful for simplification, but too risky to include by default.\<close>
diff -r a0088f1c049d -r d4f459eb7ed0 src/HOL/Zorn.thy
--- a/src/HOL/Zorn.thy	Fri May 27 23:35:13 2016 +0200
+++ b/src/HOL/Zorn.thy	Fri May 27 23:58:24 2016 +0200
@@ -416,7 +416,7 @@
 
 lemma chains_extend:
   "[| c \<in> chains S; z \<in> S; \<forall>x \<in> c. x \<subseteq> (z:: 'a set) |] ==> {z} Un c \<in> chains S"
-  by (unfold chains_def chain_subset_def) blast
+  unfolding chains_def chain_subset_def by blast
 
 lemma mono_Chains: "r \<subseteq> s \<Longrightarrow> Chains r \<subseteq> Chains s"
   unfolding Chains_def by blast
@@ -453,10 +453,10 @@
 text\<open>Various other lemmas\<close>
 
 lemma chainsD: "[| c \<in> chains S; x \<in> c; y \<in> c |] ==> x \<subseteq> y | y \<subseteq> x"
-by (unfold chains_def chain_subset_def) blast
+  unfolding chains_def chain_subset_def by blast
 
 lemma chainsD2: "!!(c :: 'a set set). c \<in> chains S ==> c \<subseteq> S"
-by (unfold chains_def) blast
+  unfolding chains_def by blast
 
 lemma Zorns_po_lemma:
   assumes po: "Partial_order r"
@@ -682,11 +682,11 @@
     moreover have "Total ?m" using \<open>Total m\<close> and Fm by (auto simp: total_on_def)
     moreover have "wf (?m - Id)"
     proof -
-      have "wf ?s" using \<open>x \<notin> Field m\<close> unfolding wf_eq_minimal Field_def
-        by (auto simp: Bex_def)
+      have "wf ?s" using \<open>x \<notin> Field m\<close> 
+        by (auto simp: wf_eq_minimal Field_def Bex_def)
       thus ?thesis using \<open>wf (m - Id)\<close> and \<open>x \<notin> Field m\<close>
         wf_subset [OF \<open>wf ?s\<close> Diff_subset]
-        unfolding Un_Diff Field_def by (auto intro: wf_Un)
+        by (auto simp: Un_Diff Field_def intro: wf_Un)
     qed
     ultimately have "Well_order ?m" by (simp add: order_on_defs)
 \<comment>\<open>We show that the extension is above m\<close>