--- a/src/Doc/IsarRef/HOL_Specific.thy Fri Oct 12 15:08:29 2012 +0200
+++ b/src/Doc/IsarRef/HOL_Specific.thy Fri Oct 12 18:58:20 2012 +0200
@@ -1189,7 +1189,7 @@
\medskip The following trivial example pulls a three-element type
into existence within the formal logical environment of HOL. *}
-typedef (open) three = "{(True, True), (True, False), (False, True)}"
+typedef three = "{(True, True), (True, False), (False, True)}"
by blast
definition "One = Abs_three (True, True)"
--- a/src/Doc/Tutorial/Types/Typedefs.thy Fri Oct 12 15:08:29 2012 +0200
+++ b/src/Doc/Tutorial/Types/Typedefs.thy Fri Oct 12 18:58:20 2012 +0200
@@ -69,7 +69,7 @@
It is easily represented by the first three natural numbers:
*}
-typedef (open) three = "{0::nat, 1, 2}"
+typedef three = "{0::nat, 1, 2}"
txt{*\noindent
In order to enforce that the representing set on the right-hand side is
--- a/src/HOL/Algebra/poly/UnivPoly2.thy Fri Oct 12 15:08:29 2012 +0200
+++ b/src/HOL/Algebra/poly/UnivPoly2.thy Fri Oct 12 18:58:20 2012 +0200
@@ -42,7 +42,7 @@
definition "UP = {f :: nat => 'a::zero. EX n. bound n f}"
-typedef (open) 'a up = "UP :: (nat => 'a::zero) set"
+typedef 'a up = "UP :: (nat => 'a::zero) set"
morphisms Rep_UP Abs_UP
proof -
have "bound 0 (\<lambda>_. 0::'a)" by (rule boundI) (rule refl)
--- a/src/HOL/BNF/Countable_Set.thy Fri Oct 12 15:08:29 2012 +0200
+++ b/src/HOL/BNF/Countable_Set.thy Fri Oct 12 18:58:20 2012 +0200
@@ -315,7 +315,7 @@
subsection{* The type of countable sets *}
-typedef (open) 'a cset = "{A :: 'a set. countable A}"
+typedef 'a cset = "{A :: 'a set. countable A}"
apply(rule exI[of _ "{}"]) by simp
abbreviation rcset where "rcset \<equiv> Rep_cset"
--- a/src/HOL/Code_Numeral.thy Fri Oct 12 15:08:29 2012 +0200
+++ b/src/HOL/Code_Numeral.thy Fri Oct 12 18:58:20 2012 +0200
@@ -13,7 +13,7 @@
subsection {* Datatype of target language numerals *}
-typedef (open) code_numeral = "UNIV \<Colon> nat set"
+typedef code_numeral = "UNIV \<Colon> nat set"
morphisms nat_of of_nat ..
lemma of_nat_nat_of [simp]:
--- a/src/HOL/Datatype.thy Fri Oct 12 15:08:29 2012 +0200
+++ b/src/HOL/Datatype.thy Fri Oct 12 18:58:20 2012 +0200
@@ -14,7 +14,7 @@
definition "Node = {p. EX f x k. p = (f :: nat => 'b + nat, x ::'a + nat) & f k = Inr 0}"
-typedef (open) ('a, 'b) node = "Node :: ((nat => 'b + nat) * ('a + nat)) set"
+typedef ('a, 'b) node = "Node :: ((nat => 'b + nat) * ('a + nat)) set"
morphisms Rep_Node Abs_Node
unfolding Node_def by auto
--- a/src/HOL/HOLCF/Algebraic.thy Fri Oct 12 15:08:29 2012 +0200
+++ b/src/HOL/HOLCF/Algebraic.thy Fri Oct 12 18:58:20 2012 +0200
@@ -12,7 +12,7 @@
subsection {* Type constructor for finite deflations *}
-typedef (open) 'a fin_defl = "{d::'a \<rightarrow> 'a. finite_deflation d}"
+typedef 'a fin_defl = "{d::'a \<rightarrow> 'a. finite_deflation d}"
by (fast intro: finite_deflation_bottom)
instantiation fin_defl :: (bifinite) below
@@ -74,7 +74,7 @@
subsection {* Defining algebraic deflations by ideal completion *}
-typedef (open) 'a defl = "{S::'a fin_defl set. below.ideal S}"
+typedef 'a defl = "{S::'a fin_defl set. below.ideal S}"
by (rule below.ex_ideal)
instantiation defl :: (bifinite) below
--- a/src/HOL/HOLCF/Compact_Basis.thy Fri Oct 12 15:08:29 2012 +0200
+++ b/src/HOL/HOLCF/Compact_Basis.thy Fri Oct 12 18:58:20 2012 +0200
@@ -14,7 +14,7 @@
definition "pd_basis = {S::'a compact_basis set. finite S \<and> S \<noteq> {}}"
-typedef (open) 'a pd_basis = "pd_basis :: 'a compact_basis set set"
+typedef 'a pd_basis = "pd_basis :: 'a compact_basis set set"
unfolding pd_basis_def
apply (rule_tac x="{arbitrary}" in exI)
apply simp
--- a/src/HOL/HOLCF/ConvexPD.thy Fri Oct 12 15:08:29 2012 +0200
+++ b/src/HOL/HOLCF/ConvexPD.thy Fri Oct 12 18:58:20 2012 +0200
@@ -119,7 +119,7 @@
subsection {* Type definition *}
-typedef (open) 'a convex_pd =
+typedef 'a convex_pd =
"{S::'a pd_basis set. convex_le.ideal S}"
by (rule convex_le.ex_ideal)
--- a/src/HOL/HOLCF/LowerPD.thy Fri Oct 12 15:08:29 2012 +0200
+++ b/src/HOL/HOLCF/LowerPD.thy Fri Oct 12 18:58:20 2012 +0200
@@ -74,7 +74,7 @@
subsection {* Type definition *}
-typedef (open) 'a lower_pd =
+typedef 'a lower_pd =
"{S::'a pd_basis set. lower_le.ideal S}"
by (rule lower_le.ex_ideal)
--- a/src/HOL/HOLCF/Universal.thy Fri Oct 12 15:08:29 2012 +0200
+++ b/src/HOL/HOLCF/Universal.thy Fri Oct 12 18:58:20 2012 +0200
@@ -198,7 +198,7 @@
subsection {* Defining the universal domain by ideal completion *}
-typedef (open) udom = "{S. udom.ideal S}"
+typedef udom = "{S. udom.ideal S}"
by (rule udom.ex_ideal)
instantiation udom :: below
@@ -247,7 +247,7 @@
subsection {* Compact bases of domains *}
-typedef (open) 'a compact_basis = "{x::'a::pcpo. compact x}"
+typedef 'a compact_basis = "{x::'a::pcpo. compact x}"
by auto
lemma Rep_compact_basis' [simp]: "compact (Rep_compact_basis a)"
--- a/src/HOL/HOLCF/UpperPD.thy Fri Oct 12 15:08:29 2012 +0200
+++ b/src/HOL/HOLCF/UpperPD.thy Fri Oct 12 18:58:20 2012 +0200
@@ -72,7 +72,7 @@
subsection {* Type definition *}
-typedef (open) 'a upper_pd =
+typedef 'a upper_pd =
"{S::'a pd_basis set. upper_le.ideal S}"
by (rule upper_le.ex_ideal)
--- a/src/HOL/Induct/QuoDataType.thy Fri Oct 12 15:08:29 2012 +0200
+++ b/src/HOL/Induct/QuoDataType.thy Fri Oct 12 18:58:20 2012 +0200
@@ -125,7 +125,7 @@
definition "Msg = UNIV//msgrel"
-typedef (open) msg = Msg
+typedef msg = Msg
morphisms Rep_Msg Abs_Msg
unfolding Msg_def by (auto simp add: quotient_def)
--- a/src/HOL/Induct/QuoNestedDataType.thy Fri Oct 12 15:08:29 2012 +0200
+++ b/src/HOL/Induct/QuoNestedDataType.thy Fri Oct 12 18:58:20 2012 +0200
@@ -144,7 +144,7 @@
definition "Exp = UNIV//exprel"
-typedef (open) exp = Exp
+typedef exp = Exp
morphisms Rep_Exp Abs_Exp
unfolding Exp_def by (auto simp add: quotient_def)
--- a/src/HOL/Induct/SList.thy Fri Oct 12 15:08:29 2012 +0200
+++ b/src/HOL/Induct/SList.thy Fri Oct 12 18:58:20 2012 +0200
@@ -55,7 +55,7 @@
definition "List = list (range Leaf)"
-typedef (open) 'a list = "List :: 'a item set"
+typedef 'a list = "List :: 'a item set"
morphisms Rep_List Abs_List
unfolding List_def by (blast intro: list.NIL_I)
--- a/src/HOL/Library/Bit.thy Fri Oct 12 15:08:29 2012 +0200
+++ b/src/HOL/Library/Bit.thy Fri Oct 12 18:58:20 2012 +0200
@@ -10,7 +10,7 @@
subsection {* Bits as a datatype *}
-typedef (open) bit = "UNIV :: bool set" ..
+typedef bit = "UNIV :: bool set" ..
instantiation bit :: "{zero, one}"
begin
--- a/src/HOL/Library/DAList.thy Fri Oct 12 15:08:29 2012 +0200
+++ b/src/HOL/Library/DAList.thy Fri Oct 12 18:58:20 2012 +0200
@@ -17,7 +17,7 @@
subsection {* Type @{text "('key, 'value) alist" } *}
-typedef (open) ('key, 'value) alist = "{xs :: ('key \<times> 'value) list. (distinct o map fst) xs}"
+typedef ('key, 'value) alist = "{xs :: ('key \<times> 'value) list. (distinct o map fst) xs}"
morphisms impl_of Alist
proof
show "[] \<in> {xs. (distinct o map fst) xs}" by simp
--- a/src/HOL/Library/Dlist.thy Fri Oct 12 15:08:29 2012 +0200
+++ b/src/HOL/Library/Dlist.thy Fri Oct 12 18:58:20 2012 +0200
@@ -8,7 +8,7 @@
subsection {* The type of distinct lists *}
-typedef (open) 'a dlist = "{xs::'a list. distinct xs}"
+typedef 'a dlist = "{xs::'a list. distinct xs}"
morphisms list_of_dlist Abs_dlist
proof
show "[] \<in> {xs. distinct xs}" by simp
--- a/src/HOL/Library/Extended_Nat.thy Fri Oct 12 15:08:29 2012 +0200
+++ b/src/HOL/Library/Extended_Nat.thy Fri Oct 12 18:58:20 2012 +0200
@@ -25,7 +25,7 @@
infinity.
*}
-typedef (open) enat = "UNIV :: nat option set" ..
+typedef enat = "UNIV :: nat option set" ..
definition enat :: "nat \<Rightarrow> enat" where
"enat n = Abs_enat (Some n)"
--- a/src/HOL/Library/FinFun.thy Fri Oct 12 15:08:29 2012 +0200
+++ b/src/HOL/Library/FinFun.thy Fri Oct 12 18:58:20 2012 +0200
@@ -83,7 +83,7 @@
definition "finfun = {f::'a\<Rightarrow>'b. \<exists>b. finite {a. f a \<noteq> b}}"
-typedef (open) ('a,'b) finfun ("(_ =>f /_)" [22, 21] 21) = "finfun :: ('a => 'b) set"
+typedef ('a,'b) finfun ("(_ =>f /_)" [22, 21] 21) = "finfun :: ('a => 'b) set"
morphisms finfun_apply Abs_finfun
proof -
have "\<exists>f. finite {x. f x \<noteq> undefined}"
--- a/src/HOL/Library/Float.thy Fri Oct 12 15:08:29 2012 +0200
+++ b/src/HOL/Library/Float.thy Fri Oct 12 18:58:20 2012 +0200
@@ -11,7 +11,7 @@
definition "float = {m * 2 powr e | (m :: int) (e :: int). True}"
-typedef (open) float = float
+typedef float = float
morphisms real_of_float float_of
unfolding float_def by auto
--- a/src/HOL/Library/Formal_Power_Series.thy Fri Oct 12 15:08:29 2012 +0200
+++ b/src/HOL/Library/Formal_Power_Series.thy Fri Oct 12 18:58:20 2012 +0200
@@ -11,7 +11,7 @@
subsection {* The type of formal power series*}
-typedef (open) 'a fps = "{f :: nat \<Rightarrow> 'a. True}"
+typedef 'a fps = "{f :: nat \<Rightarrow> 'a. True}"
morphisms fps_nth Abs_fps
by simp
--- a/src/HOL/Library/Fraction_Field.thy Fri Oct 12 15:08:29 2012 +0200
+++ b/src/HOL/Library/Fraction_Field.thy Fri Oct 12 18:58:20 2012 +0200
@@ -55,7 +55,7 @@
definition "fract = {(x::'a\<times>'a). snd x \<noteq> (0::'a::idom)} // fractrel"
-typedef (open) 'a fract = "fract :: ('a * 'a::idom) set set"
+typedef 'a fract = "fract :: ('a * 'a::idom) set set"
unfolding fract_def
proof
have "(0::'a, 1::'a) \<in> {x. snd x \<noteq> 0}" by simp
--- a/src/HOL/Library/Mapping.thy Fri Oct 12 15:08:29 2012 +0200
+++ b/src/HOL/Library/Mapping.thy Fri Oct 12 18:58:20 2012 +0200
@@ -8,7 +8,7 @@
subsection {* Type definition and primitive operations *}
-typedef (open) ('a, 'b) mapping = "UNIV :: ('a \<rightharpoonup> 'b) set"
+typedef ('a, 'b) mapping = "UNIV :: ('a \<rightharpoonup> 'b) set"
morphisms lookup Mapping ..
lemma lookup_Mapping [simp]:
--- a/src/HOL/Library/Multiset.thy Fri Oct 12 15:08:29 2012 +0200
+++ b/src/HOL/Library/Multiset.thy Fri Oct 12 18:58:20 2012 +0200
@@ -12,7 +12,7 @@
definition "multiset = {f :: 'a => nat. finite {x. f x > 0}}"
-typedef (open) 'a multiset = "multiset :: ('a => nat) set"
+typedef 'a multiset = "multiset :: ('a => nat) set"
morphisms count Abs_multiset
unfolding multiset_def
proof
--- a/src/HOL/Library/Numeral_Type.thy Fri Oct 12 15:08:29 2012 +0200
+++ b/src/HOL/Library/Numeral_Type.thy Fri Oct 12 18:58:20 2012 +0200
@@ -10,16 +10,16 @@
subsection {* Numeral Types *}
-typedef (open) num0 = "UNIV :: nat set" ..
-typedef (open) num1 = "UNIV :: unit set" ..
+typedef num0 = "UNIV :: nat set" ..
+typedef num1 = "UNIV :: unit set" ..
-typedef (open) 'a bit0 = "{0 ..< 2 * int CARD('a::finite)}"
+typedef 'a bit0 = "{0 ..< 2 * int CARD('a::finite)}"
proof
show "0 \<in> {0 ..< 2 * int CARD('a)}"
by simp
qed
-typedef (open) 'a bit1 = "{0 ..< 1 + 2 * int CARD('a::finite)}"
+typedef 'a bit1 = "{0 ..< 1 + 2 * int CARD('a::finite)}"
proof
show "0 \<in> {0 ..< 1 + 2 * int CARD('a)}"
by simp
--- a/src/HOL/Library/Polynomial.thy Fri Oct 12 15:08:29 2012 +0200
+++ b/src/HOL/Library/Polynomial.thy Fri Oct 12 18:58:20 2012 +0200
@@ -13,7 +13,7 @@
definition "Poly = {f::nat \<Rightarrow> 'a::zero. \<exists>n. \<forall>i>n. f i = 0}"
-typedef (open) 'a poly = "Poly :: (nat => 'a::zero) set"
+typedef 'a poly = "Poly :: (nat => 'a::zero) set"
morphisms coeff Abs_poly
unfolding Poly_def by auto
--- a/src/HOL/Library/Quotient_Type.thy Fri Oct 12 15:08:29 2012 +0200
+++ b/src/HOL/Library/Quotient_Type.thy Fri Oct 12 18:58:20 2012 +0200
@@ -60,7 +60,7 @@
definition "quot = {{x. a \<sim> x} | a::'a::eqv. True}"
-typedef (open) 'a quot = "quot :: 'a::eqv set set"
+typedef 'a quot = "quot :: 'a::eqv set set"
unfolding quot_def by blast
lemma quotI [intro]: "{x. a \<sim> x} \<in> quot"
--- a/src/HOL/Library/RBT.thy Fri Oct 12 15:08:29 2012 +0200
+++ b/src/HOL/Library/RBT.thy Fri Oct 12 18:58:20 2012 +0200
@@ -10,7 +10,7 @@
subsection {* Type definition *}
-typedef (open) ('a, 'b) rbt = "{t :: ('a\<Colon>linorder, 'b) RBT_Impl.rbt. is_rbt t}"
+typedef ('a, 'b) rbt = "{t :: ('a\<Colon>linorder, 'b) RBT_Impl.rbt. is_rbt t}"
morphisms impl_of RBT
proof -
have "RBT_Impl.Empty \<in> ?rbt" by simp
--- a/src/HOL/Library/Saturated.thy Fri Oct 12 15:08:29 2012 +0200
+++ b/src/HOL/Library/Saturated.thy Fri Oct 12 18:58:20 2012 +0200
@@ -12,7 +12,7 @@
subsection {* The type of saturated naturals *}
-typedef (open) ('a::len) sat = "{.. len_of TYPE('a)}"
+typedef ('a::len) sat = "{.. len_of TYPE('a)}"
morphisms nat_of Abs_sat
by auto
--- a/src/HOL/Library/Target_Numeral.thy Fri Oct 12 15:08:29 2012 +0200
+++ b/src/HOL/Library/Target_Numeral.thy Fri Oct 12 18:58:20 2012 +0200
@@ -4,7 +4,7 @@
subsection {* Type of target language numerals *}
-typedef (open) int = "UNIV \<Colon> int set"
+typedef int = "UNIV \<Colon> int set"
morphisms int_of of_int ..
hide_type (open) int
--- a/src/HOL/Limits.thy Fri Oct 12 15:08:29 2012 +0200
+++ b/src/HOL/Limits.thy Fri Oct 12 18:58:20 2012 +0200
@@ -20,7 +20,7 @@
assumes conj: "F (\<lambda>x. P x) \<Longrightarrow> F (\<lambda>x. Q x) \<Longrightarrow> F (\<lambda>x. P x \<and> Q x)"
assumes mono: "\<forall>x. P x \<longrightarrow> Q x \<Longrightarrow> F (\<lambda>x. P x) \<Longrightarrow> F (\<lambda>x. Q x)"
-typedef (open) 'a filter = "{F :: ('a \<Rightarrow> bool) \<Rightarrow> bool. is_filter F}"
+typedef 'a filter = "{F :: ('a \<Rightarrow> bool) \<Rightarrow> bool. is_filter F}"
proof
show "(\<lambda>x. True) \<in> ?filter" by (auto intro: is_filter.intro)
qed
--- a/src/HOL/Matrix_LP/Matrix.thy Fri Oct 12 15:08:29 2012 +0200
+++ b/src/HOL/Matrix_LP/Matrix.thy Fri Oct 12 18:58:20 2012 +0200
@@ -13,7 +13,7 @@
definition "matrix = {(f::(nat \<Rightarrow> nat \<Rightarrow> 'a::zero)). finite (nonzero_positions f)}"
-typedef (open) 'a matrix = "matrix :: (nat \<Rightarrow> nat \<Rightarrow> 'a::zero) set"
+typedef 'a matrix = "matrix :: (nat \<Rightarrow> nat \<Rightarrow> 'a::zero) set"
unfolding matrix_def
proof
show "(\<lambda>j i. 0) \<in> {(f::(nat \<Rightarrow> nat \<Rightarrow> 'a::zero)). finite (nonzero_positions f)}"
--- a/src/HOL/Multivariate_Analysis/Finite_Cartesian_Product.thy Fri Oct 12 15:08:29 2012 +0200
+++ b/src/HOL/Multivariate_Analysis/Finite_Cartesian_Product.thy Fri Oct 12 18:58:20 2012 +0200
@@ -13,7 +13,7 @@
subsection {* Finite Cartesian products, with indexing and lambdas. *}
-typedef (open) ('a, 'b) vec = "UNIV :: (('b::finite) \<Rightarrow> 'a) set"
+typedef ('a, 'b) vec = "UNIV :: (('b::finite) \<Rightarrow> 'a) set"
morphisms vec_nth vec_lambda ..
notation
--- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Fri Oct 12 15:08:29 2012 +0200
+++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Fri Oct 12 18:58:20 2012 +0200
@@ -13,7 +13,7 @@
subsection {* General notion of a topology as a value *}
definition "istopology L \<longleftrightarrow> L {} \<and> (\<forall>S T. L S \<longrightarrow> L T \<longrightarrow> L (S \<inter> T)) \<and> (\<forall>K. Ball K L \<longrightarrow> L (\<Union> K))"
-typedef (open) 'a topology = "{L::('a set) \<Rightarrow> bool. istopology L}"
+typedef 'a topology = "{L::('a set) \<Rightarrow> bool. istopology L}"
morphisms "openin" "topology"
unfolding istopology_def by blast
--- a/src/HOL/NSA/StarDef.thy Fri Oct 12 15:08:29 2012 +0200
+++ b/src/HOL/NSA/StarDef.thy Fri Oct 12 18:58:20 2012 +0200
@@ -40,7 +40,7 @@
definition "star = (UNIV :: (nat \<Rightarrow> 'a) set) // starrel"
-typedef (open) 'a star = "star :: (nat \<Rightarrow> 'a) set set"
+typedef 'a star = "star :: (nat \<Rightarrow> 'a) set set"
unfolding star_def by (auto intro: quotientI)
definition
--- a/src/HOL/Nat.thy Fri Oct 12 15:08:29 2012 +0200
+++ b/src/HOL/Nat.thy Fri Oct 12 18:58:20 2012 +0200
@@ -33,7 +33,7 @@
Zero_RepI: "Nat Zero_Rep"
| Suc_RepI: "Nat i \<Longrightarrow> Nat (Suc_Rep i)"
-typedef (open) nat = "{n. Nat n}"
+typedef nat = "{n. Nat n}"
morphisms Rep_Nat Abs_Nat
using Nat.Zero_RepI by auto
--- a/src/HOL/Nitpick_Examples/Manual_Nits.thy Fri Oct 12 15:08:29 2012 +0200
+++ b/src/HOL/Nitpick_Examples/Manual_Nits.thy Fri Oct 12 18:58:20 2012 +0200
@@ -95,7 +95,7 @@
subsection {* 2.7. Typedefs, Records, Rationals, and Reals *}
definition "three = {0\<Colon>nat, 1, 2}"
-typedef (open) three = three
+typedef three = three
unfolding three_def by blast
definition A :: three where "A \<equiv> Abs_three 0"
@@ -201,7 +201,7 @@
(* BEGIN LAZY LIST SETUP *)
definition "llist = (UNIV\<Colon>('a list + (nat \<Rightarrow> 'a)) set)"
-typedef (open) 'a llist = "llist\<Colon>('a list + (nat \<Rightarrow> 'a)) set"
+typedef 'a llist = "llist\<Colon>('a list + (nat \<Rightarrow> 'a)) set"
unfolding llist_def by auto
definition LNil where
--- a/src/HOL/Nitpick_Examples/Refute_Nits.thy Fri Oct 12 15:08:29 2012 +0200
+++ b/src/HOL/Nitpick_Examples/Refute_Nits.thy Fri Oct 12 18:58:20 2012 +0200
@@ -541,7 +541,7 @@
definition "myTdef = insert (undefined::'a) (undefined::'a set)"
-typedef (open) 'a myTdef = "myTdef :: 'a set"
+typedef 'a myTdef = "myTdef :: 'a set"
unfolding myTdef_def by auto
lemma "(x\<Colon>'a myTdef) = y"
@@ -552,7 +552,7 @@
definition "T_bij = {(f::'a\<Rightarrow>'a). \<forall>y. \<exists>!x. f x = y}"
-typedef (open) 'a T_bij = "T_bij :: ('a \<Rightarrow> 'a) set"
+typedef 'a T_bij = "T_bij :: ('a \<Rightarrow> 'a) set"
unfolding T_bij_def by auto
lemma "P (f\<Colon>(myTdecl myTdef) T_bij)"
--- a/src/HOL/Nitpick_Examples/Typedef_Nits.thy Fri Oct 12 15:08:29 2012 +0200
+++ b/src/HOL/Nitpick_Examples/Typedef_Nits.thy Fri Oct 12 18:58:20 2012 +0200
@@ -15,7 +15,7 @@
timeout = 240]
definition "three = {0\<Colon>nat, 1, 2}"
-typedef (open) three = three
+typedef three = three
unfolding three_def by blast
definition A :: three where "A \<equiv> Abs_three 0"
@@ -28,7 +28,7 @@
definition "one_or_two = {undefined False\<Colon>'a, undefined True}"
-typedef (open) 'a one_or_two = "one_or_two :: 'a set"
+typedef 'a one_or_two = "one_or_two :: 'a set"
unfolding one_or_two_def by auto
lemma "x = (y\<Colon>unit one_or_two)"
@@ -54,7 +54,7 @@
definition "bounded = {n\<Colon>nat. finite (UNIV \<Colon> 'a set) \<longrightarrow> n < card (UNIV \<Colon> 'a set)}"
-typedef (open) 'a bounded = "bounded(TYPE('a))"
+typedef 'a bounded = "bounded(TYPE('a))"
unfolding bounded_def
apply (rule_tac x = 0 in exI)
apply (case_tac "card UNIV = 0")
--- a/src/HOL/Nominal/Nominal.thy Fri Oct 12 15:08:29 2012 +0200
+++ b/src/HOL/Nominal/Nominal.thy Fri Oct 12 18:58:20 2012 +0200
@@ -3376,7 +3376,7 @@
definition "ABS = ABS_set"
-typedef (open) ('x,'a) ABS ("\<guillemotleft>_\<guillemotright>_" [1000,1000] 1000) =
+typedef ('x,'a) ABS ("\<guillemotleft>_\<guillemotright>_" [1000,1000] 1000) =
"ABS::('x\<Rightarrow>('a noption)) set"
morphisms Rep_ABS Abs_ABS
unfolding ABS_def
--- a/src/HOL/Probability/Sigma_Algebra.thy Fri Oct 12 15:08:29 2012 +0200
+++ b/src/HOL/Probability/Sigma_Algebra.thy Fri Oct 12 18:58:20 2012 +0200
@@ -997,7 +997,7 @@
definition measure_space :: "'a set \<Rightarrow> 'a set set \<Rightarrow> ('a set \<Rightarrow> ereal) \<Rightarrow> bool" where
"measure_space \<Omega> A \<mu> \<longleftrightarrow> sigma_algebra \<Omega> A \<and> positive A \<mu> \<and> countably_additive A \<mu>"
-typedef (open) 'a measure = "{(\<Omega>::'a set, A, \<mu>). (\<forall>a\<in>-A. \<mu> a = 0) \<and> measure_space \<Omega> A \<mu> }"
+typedef 'a measure = "{(\<Omega>::'a set, A, \<mu>). (\<forall>a\<in>-A. \<mu> a = 0) \<and> measure_space \<Omega> A \<mu> }"
proof
have "sigma_algebra UNIV {{}, UNIV}"
by (auto simp: sigma_algebra_iff2)
--- a/src/HOL/Product_Type.thy Fri Oct 12 15:08:29 2012 +0200
+++ b/src/HOL/Product_Type.thy Fri Oct 12 18:58:20 2012 +0200
@@ -43,7 +43,7 @@
subsection {* The @{text unit} type *}
-typedef (open) unit = "{True}"
+typedef unit = "{True}"
by auto
definition Unity :: unit ("'(')")
@@ -132,7 +132,7 @@
definition "prod = {f. \<exists>a b. f = Pair_Rep (a\<Colon>'a) (b\<Colon>'b)}"
-typedef (open) ('a, 'b) prod (infixr "*" 20) = "prod :: ('a \<Rightarrow> 'b \<Rightarrow> bool) set"
+typedef ('a, 'b) prod (infixr "*" 20) = "prod :: ('a \<Rightarrow> 'b \<Rightarrow> bool) set"
unfolding prod_def by auto
type_notation (xsymbols)
--- a/src/HOL/Quickcheck_Narrowing.thy Fri Oct 12 15:08:29 2012 +0200
+++ b/src/HOL/Quickcheck_Narrowing.thy Fri Oct 12 18:58:20 2012 +0200
@@ -25,7 +25,7 @@
subsubsection {* Type @{text "code_int"} for Haskell Quickcheck's Int type *}
-typedef (open) code_int = "UNIV \<Colon> int set"
+typedef code_int = "UNIV \<Colon> int set"
morphisms int_of of_int by rule
lemma of_int_int_of [simp]:
--- a/src/HOL/Quotient_Examples/Lift_DList.thy Fri Oct 12 15:08:29 2012 +0200
+++ b/src/HOL/Quotient_Examples/Lift_DList.thy Fri Oct 12 18:58:20 2012 +0200
@@ -8,7 +8,7 @@
subsection {* The type of distinct lists *}
-typedef (open) 'a dlist = "{xs::'a list. distinct xs}"
+typedef 'a dlist = "{xs::'a list. distinct xs}"
morphisms list_of_dlist Abs_dlist
proof
show "[] \<in> {xs. distinct xs}" by simp
--- a/src/HOL/Quotient_Examples/Lift_Set.thy Fri Oct 12 15:08:29 2012 +0200
+++ b/src/HOL/Quotient_Examples/Lift_Set.thy Fri Oct 12 18:58:20 2012 +0200
@@ -10,7 +10,7 @@
definition set where "set = (UNIV :: ('a \<Rightarrow> bool) set)"
-typedef (open) 'a set = "set :: ('a \<Rightarrow> bool) set"
+typedef 'a set = "set :: ('a \<Rightarrow> bool) set"
morphisms member Set
unfolding set_def by auto
--- a/src/HOL/SMT_Examples/SMT_Tests.thy Fri Oct 12 15:08:29 2012 +0200
+++ b/src/HOL/SMT_Examples/SMT_Tests.thy Fri Oct 12 18:58:20 2012 +0200
@@ -760,7 +760,7 @@
definition "three = {1, 2, 3::int}"
-typedef (open) three = three
+typedef three = three
unfolding three_def by auto
definition n1 where "n1 = Abs_three 1"
--- a/src/HOL/String.thy Fri Oct 12 15:08:29 2012 +0200
+++ b/src/HOL/String.thy Fri Oct 12 18:58:20 2012 +0200
@@ -152,7 +152,7 @@
subsection {* Strings as dedicated type *}
-typedef (open) literal = "UNIV :: string set"
+typedef literal = "UNIV :: string set"
morphisms explode STR ..
instantiation literal :: size
--- a/src/HOL/Sum_Type.thy Fri Oct 12 15:08:29 2012 +0200
+++ b/src/HOL/Sum_Type.thy Fri Oct 12 18:58:20 2012 +0200
@@ -19,7 +19,7 @@
definition "sum = {f. (\<exists>a. f = Inl_Rep (a::'a)) \<or> (\<exists>b. f = Inr_Rep (b::'b))}"
-typedef (open) ('a, 'b) sum (infixr "+" 10) = "sum :: ('a => 'b => bool => bool) set"
+typedef ('a, 'b) sum (infixr "+" 10) = "sum :: ('a => 'b => bool => bool) set"
unfolding sum_def by auto
lemma Inl_RepI: "Inl_Rep a \<in> sum"
--- a/src/HOL/Tools/typedef.ML Fri Oct 12 15:08:29 2012 +0200
+++ b/src/HOL/Tools/typedef.ML Fri Oct 12 18:58:20 2012 +0200
@@ -276,17 +276,12 @@
val _ =
Outer_Syntax.local_theory_to_proof @{command_spec "typedef"}
"HOL type definition (requires non-emptiness proof)"
- (Scan.optional (@{keyword "("} |--
- ((@{keyword "open"} >> K false) -- Scan.option Parse.binding ||
- Parse.binding >> (fn s => (true, SOME s))) --| @{keyword ")"}) (true, NONE) --
+ (Scan.option (@{keyword "("} |-- Parse.binding --| @{keyword ")"}) --
(Parse.type_args_constrained -- Parse.binding) --
Parse.opt_mixfix -- (@{keyword "="} |-- Parse.term) --
Scan.option (@{keyword "morphisms"} |-- Parse.!!! (Parse.binding -- Parse.binding))
- >> (fn ((((((def, opt_name), (args, t)), mx), A), morphs)) => fn lthy =>
- (if def then
- error "typedef with implicit set definition -- use \"typedef (open)\" instead"
- else ();
- typedef_cmd (the_default t opt_name, (t, args, mx), A, morphs) lthy)));
+ >> (fn (((((opt_name, (args, t)), mx), A), morphs)) => fn lthy =>
+ typedef_cmd (the_default t opt_name, (t, args, mx), A, morphs) lthy));
end;
--- a/src/HOL/UNITY/UNITY.thy Fri Oct 12 15:08:29 2012 +0200
+++ b/src/HOL/UNITY/UNITY.thy Fri Oct 12 18:58:20 2012 +0200
@@ -17,7 +17,7 @@
{(init:: 'a set, acts :: ('a * 'a)set set,
allowed :: ('a * 'a)set set). Id \<in> acts & Id: allowed}"
-typedef (open) 'a program = "Program :: ('a set * ('a * 'a) set set * ('a * 'a) set set) set"
+typedef 'a program = "Program :: ('a set * ('a * 'a) set set * ('a * 'a) set set) set"
morphisms Rep_Program Abs_Program
unfolding Program_def by blast
--- a/src/HOL/Word/Word.thy Fri Oct 12 15:08:29 2012 +0200
+++ b/src/HOL/Word/Word.thy Fri Oct 12 18:58:20 2012 +0200
@@ -16,7 +16,7 @@
subsection {* Type definition *}
-typedef (open) 'a word = "{(0::int) ..< 2^len_of TYPE('a::len0)}"
+typedef 'a word = "{(0::int) ..< 2^len_of TYPE('a::len0)}"
morphisms uint Abs_word by auto
lemma uint_nonnegative:
--- a/src/HOL/ZF/Games.thy Fri Oct 12 15:08:29 2012 +0200
+++ b/src/HOL/ZF/Games.thy Fri Oct 12 18:58:20 2012 +0200
@@ -191,7 +191,7 @@
definition "game = games_lfp"
-typedef (open) game = game
+typedef game = game
unfolding game_def by (blast intro: games_lfp_nonempty)
definition left_options :: "game \<Rightarrow> game zet" where
@@ -843,7 +843,7 @@
definition "Pg = UNIV//eq_game_rel"
-typedef (open) Pg = Pg
+typedef Pg = Pg
unfolding Pg_def by (auto simp add: quotient_def)
lemma equiv_eq_game[simp]: "equiv UNIV eq_game_rel"
--- a/src/HOL/ZF/Zet.thy Fri Oct 12 15:08:29 2012 +0200
+++ b/src/HOL/ZF/Zet.thy Fri Oct 12 18:58:20 2012 +0200
@@ -11,7 +11,7 @@
definition "zet = {A :: 'a set | A f z. inj_on f A \<and> f ` A \<subseteq> explode z}"
-typedef (open) 'a zet = "zet :: 'a set set"
+typedef 'a zet = "zet :: 'a set set"
unfolding zet_def by blast
definition zin :: "'a \<Rightarrow> 'a zet \<Rightarrow> bool" where
--- a/src/HOL/ex/Dedekind_Real.thy Fri Oct 12 15:08:29 2012 +0200
+++ b/src/HOL/ex/Dedekind_Real.thy Fri Oct 12 18:58:20 2012 +0200
@@ -46,7 +46,7 @@
definition "preal = {A. cut A}"
-typedef (open) preal = preal
+typedef preal = preal
unfolding preal_def by (blast intro: cut_of_rat [OF zero_less_one])
definition
@@ -1171,7 +1171,7 @@
definition "Real = UNIV//realrel"
-typedef (open) real = Real
+typedef real = Real
morphisms Rep_Real Abs_Real
unfolding Real_def by (auto simp add: quotient_def)
--- a/src/HOL/ex/Executable_Relation.thy Fri Oct 12 15:08:29 2012 +0200
+++ b/src/HOL/ex/Executable_Relation.thy Fri Oct 12 18:58:20 2012 +0200
@@ -6,7 +6,7 @@
subsubsection {* Definition of the dedicated type for relations *}
-typedef (open) 'a rel = "UNIV :: (('a * 'a) set) set"
+typedef 'a rel = "UNIV :: (('a * 'a) set) set"
morphisms set_of_rel rel_of_set by simp
setup_lifting type_definition_rel
--- a/src/HOL/ex/PER.thy Fri Oct 12 15:08:29 2012 +0200
+++ b/src/HOL/ex/PER.thy Fri Oct 12 18:58:20 2012 +0200
@@ -153,7 +153,7 @@
definition "quot = {{x. a \<sim> x}| a::'a::partial_equiv. True}"
-typedef (open) 'a quot = "quot :: 'a::partial_equiv set set"
+typedef 'a quot = "quot :: 'a::partial_equiv set set"
unfolding quot_def by blast
lemma quotI [intro]: "{x. a \<sim> x} \<in> quot"
--- a/src/HOL/ex/Refute_Examples.thy Fri Oct 12 15:08:29 2012 +0200
+++ b/src/HOL/ex/Refute_Examples.thy Fri Oct 12 18:58:20 2012 +0200
@@ -485,7 +485,7 @@
definition "myTdef = insert (undefined::'a) (undefined::'a set)"
-typedef (open) 'a myTdef = "myTdef :: 'a set"
+typedef 'a myTdef = "myTdef :: 'a set"
unfolding myTdef_def by auto
lemma "(x::'a myTdef) = y"
@@ -496,7 +496,7 @@
definition "T_bij = {(f::'a\<Rightarrow>'a). \<forall>y. \<exists>!x. f x = y}"
-typedef (open) 'a T_bij = "T_bij :: ('a \<Rightarrow> 'a) set"
+typedef 'a T_bij = "T_bij :: ('a \<Rightarrow> 'a) set"
unfolding T_bij_def by auto
lemma "P (f::(myTdecl myTdef) T_bij)"