# HG changeset patch
# User huffman
# Date 1291264179 28800
# Node ID 28cd51cff70c8be45ea3c48d8793f981f137a451
# Parent  f2c9ebbe04aaeb514348bab1fb50654f6b0beb94
reformulate lemma preorder.ex_ideal, and use it for typedefs

diff -r f2c9ebbe04aa -r 28cd51cff70c src/HOL/HOLCF/Algebraic.thy
--- a/src/HOL/HOLCF/Algebraic.thy	Wed Dec 01 06:50:54 2010 -0800
+++ b/src/HOL/HOLCF/Algebraic.thy	Wed Dec 01 20:29:39 2010 -0800
@@ -73,7 +73,7 @@
 subsection {* Defining algebraic deflations by ideal completion *}
 
 typedef (open) defl = "{S::fin_defl set. below.ideal S}"
-by (fast intro: below.ideal_principal)
+by (rule below.ex_ideal)
 
 instantiation defl :: below
 begin
diff -r f2c9ebbe04aa -r 28cd51cff70c src/HOL/HOLCF/Completion.thy
--- a/src/HOL/HOLCF/Completion.thy	Wed Dec 01 06:50:54 2010 -0800
+++ b/src/HOL/HOLCF/Completion.thy	Wed Dec 01 20:29:39 2010 -0800
@@ -49,8 +49,8 @@
 apply (fast intro: r_trans)
 done
 
-lemma ex_ideal: "\<exists>A. ideal A"
-by (rule exI, rule ideal_principal)
+lemma ex_ideal: "\<exists>A. A \<in> {A. ideal A}"
+by (fast intro: ideal_principal)
 
 lemma lub_image_principal:
   assumes f: "\<And>x y. x \<preceq> y \<Longrightarrow> f x \<sqsubseteq> f y"
diff -r f2c9ebbe04aa -r 28cd51cff70c src/HOL/HOLCF/ConvexPD.thy
--- a/src/HOL/HOLCF/ConvexPD.thy	Wed Dec 01 06:50:54 2010 -0800
+++ b/src/HOL/HOLCF/ConvexPD.thy	Wed Dec 01 20:29:39 2010 -0800
@@ -121,7 +121,7 @@
 
 typedef (open) 'a convex_pd =
   "{S::'a pd_basis set. convex_le.ideal S}"
-by (fast intro: convex_le.ideal_principal)
+by (rule convex_le.ex_ideal)
 
 instantiation convex_pd :: ("domain") below
 begin
diff -r f2c9ebbe04aa -r 28cd51cff70c src/HOL/HOLCF/LowerPD.thy
--- a/src/HOL/HOLCF/LowerPD.thy	Wed Dec 01 06:50:54 2010 -0800
+++ b/src/HOL/HOLCF/LowerPD.thy	Wed Dec 01 20:29:39 2010 -0800
@@ -76,7 +76,7 @@
 
 typedef (open) 'a lower_pd =
   "{S::'a pd_basis set. lower_le.ideal S}"
-by (fast intro: lower_le.ideal_principal)
+by (rule lower_le.ex_ideal)
 
 instantiation lower_pd :: ("domain") below
 begin
diff -r f2c9ebbe04aa -r 28cd51cff70c src/HOL/HOLCF/Universal.thy
--- a/src/HOL/HOLCF/Universal.thy	Wed Dec 01 06:50:54 2010 -0800
+++ b/src/HOL/HOLCF/Universal.thy	Wed Dec 01 20:29:39 2010 -0800
@@ -199,7 +199,7 @@
 subsection {* Defining the universal domain by ideal completion *}
 
 typedef (open) udom = "{S. udom.ideal S}"
-by (fast intro: udom.ideal_principal)
+by (rule udom.ex_ideal)
 
 instantiation udom :: below
 begin
diff -r f2c9ebbe04aa -r 28cd51cff70c src/HOL/HOLCF/UpperPD.thy
--- a/src/HOL/HOLCF/UpperPD.thy	Wed Dec 01 06:50:54 2010 -0800
+++ b/src/HOL/HOLCF/UpperPD.thy	Wed Dec 01 20:29:39 2010 -0800
@@ -74,7 +74,7 @@
 
 typedef (open) 'a upper_pd =
   "{S::'a pd_basis set. upper_le.ideal S}"
-by (fast intro: upper_le.ideal_principal)
+by (rule upper_le.ex_ideal)
 
 instantiation upper_pd :: ("domain") below
 begin