Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Library/Complete_Partial_Order2.thy
changeset 63170 eae6549dbea2
parent 63092 a949b2a5f51d
child 63243 1bc6816fd525 
--- a/src/HOL/Library/Complete_Partial_Order2.thy	Fri May 27 20:13:06 2016 +0200
+++ b/src/HOL/Library/Complete_Partial_Order2.thy	Fri May 27 20:23:55 2016 +0200
@@ -308,7 +308,8 @@
   fix x y
   assume "x \<sqsubseteq> y"
   show "?fixp x \<le> ?fixp y"
-    unfolding ccpo.fixp_def[OF ccpo_fun] fun_lub_apply using chain
+    apply (simp only: ccpo.fixp_def[OF ccpo_fun] fun_lub_apply)
+    using chain
   proof(rule ccpo_Sup_least)
     fix x'
     assume "x' \<in> (\<lambda>f. f x) ` ?iter"
@@ -599,7 +600,8 @@
     fix x y
     assume "x \<sqsubseteq> y"
     show "?fixp x \<le> ?fixp y"
-      unfolding ccpo.fixp_def[OF ccpo_fun] fun_lub_apply using chain
+      apply (simp only: ccpo.fixp_def[OF ccpo_fun] fun_lub_apply)
+      using chain
     proof(rule ccpo_Sup_least)
       fix x'
       assume "x' \<in> (\<lambda>f. f x) ` ?iter"
isabelle