discontinued obsolete typedef (open) syntax;
authorwenzelm
Fri Oct 12 18:58:20 2012 +0200 (2012-10-12)
changeset 49834b27bbb021df1
parent 49833 1d80798e8d8a
child 49835 31f32ec4d766
discontinued obsolete typedef (open) syntax;
src/Doc/IsarRef/HOL_Specific.thy
src/Doc/Tutorial/Types/Typedefs.thy
src/HOL/Algebra/poly/UnivPoly2.thy
src/HOL/BNF/Countable_Set.thy
src/HOL/Code_Numeral.thy
src/HOL/Datatype.thy
src/HOL/HOLCF/Algebraic.thy
src/HOL/HOLCF/Compact_Basis.thy
src/HOL/HOLCF/ConvexPD.thy
src/HOL/HOLCF/LowerPD.thy
src/HOL/HOLCF/Universal.thy
src/HOL/HOLCF/UpperPD.thy
src/HOL/Induct/QuoDataType.thy
src/HOL/Induct/QuoNestedDataType.thy
src/HOL/Induct/SList.thy
src/HOL/Library/Bit.thy
src/HOL/Library/DAList.thy
src/HOL/Library/Dlist.thy
src/HOL/Library/Extended_Nat.thy
src/HOL/Library/FinFun.thy
src/HOL/Library/Float.thy
src/HOL/Library/Formal_Power_Series.thy
src/HOL/Library/Fraction_Field.thy
src/HOL/Library/Mapping.thy
src/HOL/Library/Multiset.thy
src/HOL/Library/Numeral_Type.thy
src/HOL/Library/Polynomial.thy
src/HOL/Library/Quotient_Type.thy
src/HOL/Library/RBT.thy
src/HOL/Library/Saturated.thy
src/HOL/Library/Target_Numeral.thy
src/HOL/Limits.thy
src/HOL/Matrix_LP/Matrix.thy
src/HOL/Multivariate_Analysis/Finite_Cartesian_Product.thy
src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
src/HOL/NSA/StarDef.thy
src/HOL/Nat.thy
src/HOL/Nitpick_Examples/Manual_Nits.thy
src/HOL/Nitpick_Examples/Refute_Nits.thy
src/HOL/Nitpick_Examples/Typedef_Nits.thy
src/HOL/Nominal/Nominal.thy
src/HOL/Probability/Sigma_Algebra.thy
src/HOL/Product_Type.thy
src/HOL/Quickcheck_Narrowing.thy
src/HOL/Quotient_Examples/Lift_DList.thy
src/HOL/Quotient_Examples/Lift_Set.thy
src/HOL/SMT_Examples/SMT_Tests.thy
src/HOL/String.thy
src/HOL/Sum_Type.thy
src/HOL/Tools/typedef.ML
src/HOL/UNITY/UNITY.thy
src/HOL/Word/Word.thy
src/HOL/ZF/Games.thy
src/HOL/ZF/Zet.thy
src/HOL/ex/Dedekind_Real.thy
src/HOL/ex/Executable_Relation.thy
src/HOL/ex/PER.thy
src/HOL/ex/Refute_Examples.thy
     1.1 --- a/src/Doc/IsarRef/HOL_Specific.thy	Fri Oct 12 15:08:29 2012 +0200
     1.2 +++ b/src/Doc/IsarRef/HOL_Specific.thy	Fri Oct 12 18:58:20 2012 +0200
     1.3 @@ -1189,7 +1189,7 @@
     1.4    \medskip The following trivial example pulls a three-element type
     1.5    into existence within the formal logical environment of HOL. *}
     1.6  
     1.7 -typedef (open) three = "{(True, True), (True, False), (False, True)}"
     1.8 +typedef three = "{(True, True), (True, False), (False, True)}"
     1.9    by blast
    1.10  
    1.11  definition "One = Abs_three (True, True)"
     2.1 --- a/src/Doc/Tutorial/Types/Typedefs.thy	Fri Oct 12 15:08:29 2012 +0200
     2.2 +++ b/src/Doc/Tutorial/Types/Typedefs.thy	Fri Oct 12 18:58:20 2012 +0200
     2.3 @@ -69,7 +69,7 @@
     2.4  It is easily represented by the first three natural numbers:
     2.5  *}
     2.6  
     2.7 -typedef (open) three = "{0::nat, 1, 2}"
     2.8 +typedef three = "{0::nat, 1, 2}"
     2.9  
    2.10  txt{*\noindent
    2.11  In order to enforce that the representing set on the right-hand side is
     3.1 --- a/src/HOL/Algebra/poly/UnivPoly2.thy	Fri Oct 12 15:08:29 2012 +0200
     3.2 +++ b/src/HOL/Algebra/poly/UnivPoly2.thy	Fri Oct 12 18:58:20 2012 +0200
     3.3 @@ -42,7 +42,7 @@
     3.4  
     3.5  definition "UP = {f :: nat => 'a::zero. EX n. bound n f}"
     3.6  
     3.7 -typedef (open) 'a up = "UP :: (nat => 'a::zero) set"
     3.8 +typedef 'a up = "UP :: (nat => 'a::zero) set"
     3.9    morphisms Rep_UP Abs_UP
    3.10  proof -
    3.11    have "bound 0 (\<lambda>_. 0::'a)" by (rule boundI) (rule refl)
     4.1 --- a/src/HOL/BNF/Countable_Set.thy	Fri Oct 12 15:08:29 2012 +0200
     4.2 +++ b/src/HOL/BNF/Countable_Set.thy	Fri Oct 12 18:58:20 2012 +0200
     4.3 @@ -315,7 +315,7 @@
     4.4  
     4.5  subsection{*  The type of countable sets *}
     4.6  
     4.7 -typedef (open) 'a cset = "{A :: 'a set. countable A}"
     4.8 +typedef 'a cset = "{A :: 'a set. countable A}"
     4.9  apply(rule exI[of _ "{}"]) by simp
    4.10  
    4.11  abbreviation rcset where "rcset \<equiv> Rep_cset"
     5.1 --- a/src/HOL/Code_Numeral.thy	Fri Oct 12 15:08:29 2012 +0200
     5.2 +++ b/src/HOL/Code_Numeral.thy	Fri Oct 12 18:58:20 2012 +0200
     5.3 @@ -13,7 +13,7 @@
     5.4  
     5.5  subsection {* Datatype of target language numerals *}
     5.6  
     5.7 -typedef (open) code_numeral = "UNIV \<Colon> nat set"
     5.8 +typedef code_numeral = "UNIV \<Colon> nat set"
     5.9    morphisms nat_of of_nat ..
    5.10  
    5.11  lemma of_nat_nat_of [simp]:
     6.1 --- a/src/HOL/Datatype.thy	Fri Oct 12 15:08:29 2012 +0200
     6.2 +++ b/src/HOL/Datatype.thy	Fri Oct 12 18:58:20 2012 +0200
     6.3 @@ -14,7 +14,7 @@
     6.4  
     6.5  definition "Node = {p. EX f x k. p = (f :: nat => 'b + nat, x ::'a + nat) & f k = Inr 0}"
     6.6  
     6.7 -typedef (open) ('a, 'b) node = "Node :: ((nat => 'b + nat) * ('a + nat)) set"
     6.8 +typedef ('a, 'b) node = "Node :: ((nat => 'b + nat) * ('a + nat)) set"
     6.9    morphisms Rep_Node Abs_Node
    6.10    unfolding Node_def by auto
    6.11  
     7.1 --- a/src/HOL/HOLCF/Algebraic.thy	Fri Oct 12 15:08:29 2012 +0200
     7.2 +++ b/src/HOL/HOLCF/Algebraic.thy	Fri Oct 12 18:58:20 2012 +0200
     7.3 @@ -12,7 +12,7 @@
     7.4  
     7.5  subsection {* Type constructor for finite deflations *}
     7.6  
     7.7 -typedef (open) 'a fin_defl = "{d::'a \<rightarrow> 'a. finite_deflation d}"
     7.8 +typedef 'a fin_defl = "{d::'a \<rightarrow> 'a. finite_deflation d}"
     7.9  by (fast intro: finite_deflation_bottom)
    7.10  
    7.11  instantiation fin_defl :: (bifinite) below
    7.12 @@ -74,7 +74,7 @@
    7.13  
    7.14  subsection {* Defining algebraic deflations by ideal completion *}
    7.15  
    7.16 -typedef (open) 'a defl = "{S::'a fin_defl set. below.ideal S}"
    7.17 +typedef 'a defl = "{S::'a fin_defl set. below.ideal S}"
    7.18  by (rule below.ex_ideal)
    7.19  
    7.20  instantiation defl :: (bifinite) below
     8.1 --- a/src/HOL/HOLCF/Compact_Basis.thy	Fri Oct 12 15:08:29 2012 +0200
     8.2 +++ b/src/HOL/HOLCF/Compact_Basis.thy	Fri Oct 12 18:58:20 2012 +0200
     8.3 @@ -14,7 +14,7 @@
     8.4  
     8.5  definition "pd_basis = {S::'a compact_basis set. finite S \<and> S \<noteq> {}}"
     8.6  
     8.7 -typedef (open) 'a pd_basis = "pd_basis :: 'a compact_basis set set"
     8.8 +typedef 'a pd_basis = "pd_basis :: 'a compact_basis set set"
     8.9    unfolding pd_basis_def
    8.10    apply (rule_tac x="{arbitrary}" in exI)
    8.11    apply simp
     9.1 --- a/src/HOL/HOLCF/ConvexPD.thy	Fri Oct 12 15:08:29 2012 +0200
     9.2 +++ b/src/HOL/HOLCF/ConvexPD.thy	Fri Oct 12 18:58:20 2012 +0200
     9.3 @@ -119,7 +119,7 @@
     9.4  
     9.5  subsection {* Type definition *}
     9.6  
     9.7 -typedef (open) 'a convex_pd =
     9.8 +typedef 'a convex_pd =
     9.9    "{S::'a pd_basis set. convex_le.ideal S}"
    9.10  by (rule convex_le.ex_ideal)
    9.11  
    10.1 --- a/src/HOL/HOLCF/LowerPD.thy	Fri Oct 12 15:08:29 2012 +0200
    10.2 +++ b/src/HOL/HOLCF/LowerPD.thy	Fri Oct 12 18:58:20 2012 +0200
    10.3 @@ -74,7 +74,7 @@
    10.4  
    10.5  subsection {* Type definition *}
    10.6  
    10.7 -typedef (open) 'a lower_pd =
    10.8 +typedef 'a lower_pd =
    10.9    "{S::'a pd_basis set. lower_le.ideal S}"
   10.10  by (rule lower_le.ex_ideal)
   10.11  
    11.1 --- a/src/HOL/HOLCF/Universal.thy	Fri Oct 12 15:08:29 2012 +0200
    11.2 +++ b/src/HOL/HOLCF/Universal.thy	Fri Oct 12 18:58:20 2012 +0200
    11.3 @@ -198,7 +198,7 @@
    11.4  
    11.5  subsection {* Defining the universal domain by ideal completion *}
    11.6  
    11.7 -typedef (open) udom = "{S. udom.ideal S}"
    11.8 +typedef udom = "{S. udom.ideal S}"
    11.9  by (rule udom.ex_ideal)
   11.10  
   11.11  instantiation udom :: below
   11.12 @@ -247,7 +247,7 @@
   11.13  
   11.14  subsection {* Compact bases of domains *}
   11.15  
   11.16 -typedef (open) 'a compact_basis = "{x::'a::pcpo. compact x}"
   11.17 +typedef 'a compact_basis = "{x::'a::pcpo. compact x}"
   11.18  by auto
   11.19  
   11.20  lemma Rep_compact_basis' [simp]: "compact (Rep_compact_basis a)"
    12.1 --- a/src/HOL/HOLCF/UpperPD.thy	Fri Oct 12 15:08:29 2012 +0200
    12.2 +++ b/src/HOL/HOLCF/UpperPD.thy	Fri Oct 12 18:58:20 2012 +0200
    12.3 @@ -72,7 +72,7 @@
    12.4  
    12.5  subsection {* Type definition *}
    12.6  
    12.7 -typedef (open) 'a upper_pd =
    12.8 +typedef 'a upper_pd =
    12.9    "{S::'a pd_basis set. upper_le.ideal S}"
   12.10  by (rule upper_le.ex_ideal)
   12.11  
    13.1 --- a/src/HOL/Induct/QuoDataType.thy	Fri Oct 12 15:08:29 2012 +0200
    13.2 +++ b/src/HOL/Induct/QuoDataType.thy	Fri Oct 12 18:58:20 2012 +0200
    13.3 @@ -125,7 +125,7 @@
    13.4  
    13.5  definition "Msg = UNIV//msgrel"
    13.6  
    13.7 -typedef (open) msg = Msg
    13.8 +typedef msg = Msg
    13.9    morphisms Rep_Msg Abs_Msg
   13.10    unfolding Msg_def by (auto simp add: quotient_def)
   13.11  
    14.1 --- a/src/HOL/Induct/QuoNestedDataType.thy	Fri Oct 12 15:08:29 2012 +0200
    14.2 +++ b/src/HOL/Induct/QuoNestedDataType.thy	Fri Oct 12 18:58:20 2012 +0200
    14.3 @@ -144,7 +144,7 @@
    14.4  
    14.5  definition "Exp = UNIV//exprel"
    14.6  
    14.7 -typedef (open) exp = Exp
    14.8 +typedef exp = Exp
    14.9    morphisms Rep_Exp Abs_Exp
   14.10    unfolding Exp_def by (auto simp add: quotient_def)
   14.11  
    15.1 --- a/src/HOL/Induct/SList.thy	Fri Oct 12 15:08:29 2012 +0200
    15.2 +++ b/src/HOL/Induct/SList.thy	Fri Oct 12 18:58:20 2012 +0200
    15.3 @@ -55,7 +55,7 @@
    15.4  
    15.5  definition "List = list (range Leaf)"
    15.6  
    15.7 -typedef (open) 'a list = "List :: 'a item set"
    15.8 +typedef 'a list = "List :: 'a item set"
    15.9    morphisms Rep_List Abs_List
   15.10    unfolding List_def by (blast intro: list.NIL_I)
   15.11  
    16.1 --- a/src/HOL/Library/Bit.thy	Fri Oct 12 15:08:29 2012 +0200
    16.2 +++ b/src/HOL/Library/Bit.thy	Fri Oct 12 18:58:20 2012 +0200
    16.3 @@ -10,7 +10,7 @@
    16.4  
    16.5  subsection {* Bits as a datatype *}
    16.6  
    16.7 -typedef (open) bit = "UNIV :: bool set" ..
    16.8 +typedef bit = "UNIV :: bool set" ..
    16.9  
   16.10  instantiation bit :: "{zero, one}"
   16.11  begin
    17.1 --- a/src/HOL/Library/DAList.thy	Fri Oct 12 15:08:29 2012 +0200
    17.2 +++ b/src/HOL/Library/DAList.thy	Fri Oct 12 18:58:20 2012 +0200
    17.3 @@ -17,7 +17,7 @@
    17.4  
    17.5  subsection {* Type @{text "('key, 'value) alist" } *}
    17.6  
    17.7 -typedef (open) ('key, 'value) alist = "{xs :: ('key \<times> 'value) list. (distinct o map fst) xs}"
    17.8 +typedef ('key, 'value) alist = "{xs :: ('key \<times> 'value) list. (distinct o map fst) xs}"
    17.9    morphisms impl_of Alist
   17.10  proof
   17.11    show "[] \<in> {xs. (distinct o map fst) xs}" by simp
    18.1 --- a/src/HOL/Library/Dlist.thy	Fri Oct 12 15:08:29 2012 +0200
    18.2 +++ b/src/HOL/Library/Dlist.thy	Fri Oct 12 18:58:20 2012 +0200
    18.3 @@ -8,7 +8,7 @@
    18.4  
    18.5  subsection {* The type of distinct lists *}
    18.6  
    18.7 -typedef (open) 'a dlist = "{xs::'a list. distinct xs}"
    18.8 +typedef 'a dlist = "{xs::'a list. distinct xs}"
    18.9    morphisms list_of_dlist Abs_dlist
   18.10  proof
   18.11    show "[] \<in> {xs. distinct xs}" by simp
    19.1 --- a/src/HOL/Library/Extended_Nat.thy	Fri Oct 12 15:08:29 2012 +0200
    19.2 +++ b/src/HOL/Library/Extended_Nat.thy	Fri Oct 12 18:58:20 2012 +0200
    19.3 @@ -25,7 +25,7 @@
    19.4    infinity.
    19.5  *}
    19.6  
    19.7 -typedef (open) enat = "UNIV :: nat option set" ..
    19.8 +typedef enat = "UNIV :: nat option set" ..
    19.9   
   19.10  definition enat :: "nat \<Rightarrow> enat" where
   19.11    "enat n = Abs_enat (Some n)"
    20.1 --- a/src/HOL/Library/FinFun.thy	Fri Oct 12 15:08:29 2012 +0200
    20.2 +++ b/src/HOL/Library/FinFun.thy	Fri Oct 12 18:58:20 2012 +0200
    20.3 @@ -83,7 +83,7 @@
    20.4  
    20.5  definition "finfun = {f::'a\<Rightarrow>'b. \<exists>b. finite {a. f a \<noteq> b}}"
    20.6  
    20.7 -typedef (open) ('a,'b) finfun  ("(_ =>f /_)" [22, 21] 21) = "finfun :: ('a => 'b) set"
    20.8 +typedef ('a,'b) finfun  ("(_ =>f /_)" [22, 21] 21) = "finfun :: ('a => 'b) set"
    20.9    morphisms finfun_apply Abs_finfun
   20.10  proof -
   20.11    have "\<exists>f. finite {x. f x \<noteq> undefined}"
    21.1 --- a/src/HOL/Library/Float.thy	Fri Oct 12 15:08:29 2012 +0200
    21.2 +++ b/src/HOL/Library/Float.thy	Fri Oct 12 18:58:20 2012 +0200
    21.3 @@ -11,7 +11,7 @@
    21.4  
    21.5  definition "float = {m * 2 powr e | (m :: int) (e :: int). True}"
    21.6  
    21.7 -typedef (open) float = float
    21.8 +typedef float = float
    21.9    morphisms real_of_float float_of
   21.10    unfolding float_def by auto
   21.11  
    22.1 --- a/src/HOL/Library/Formal_Power_Series.thy	Fri Oct 12 15:08:29 2012 +0200
    22.2 +++ b/src/HOL/Library/Formal_Power_Series.thy	Fri Oct 12 18:58:20 2012 +0200
    22.3 @@ -11,7 +11,7 @@
    22.4  
    22.5  subsection {* The type of formal power series*}
    22.6  
    22.7 -typedef (open) 'a fps = "{f :: nat \<Rightarrow> 'a. True}"
    22.8 +typedef 'a fps = "{f :: nat \<Rightarrow> 'a. True}"
    22.9    morphisms fps_nth Abs_fps
   22.10    by simp
   22.11  
    23.1 --- a/src/HOL/Library/Fraction_Field.thy	Fri Oct 12 15:08:29 2012 +0200
    23.2 +++ b/src/HOL/Library/Fraction_Field.thy	Fri Oct 12 18:58:20 2012 +0200
    23.3 @@ -55,7 +55,7 @@
    23.4  
    23.5  definition "fract = {(x::'a\<times>'a). snd x \<noteq> (0::'a::idom)} // fractrel"
    23.6  
    23.7 -typedef (open) 'a fract = "fract :: ('a * 'a::idom) set set"
    23.8 +typedef 'a fract = "fract :: ('a * 'a::idom) set set"
    23.9    unfolding fract_def
   23.10  proof
   23.11    have "(0::'a, 1::'a) \<in> {x. snd x \<noteq> 0}" by simp
    24.1 --- a/src/HOL/Library/Mapping.thy	Fri Oct 12 15:08:29 2012 +0200
    24.2 +++ b/src/HOL/Library/Mapping.thy	Fri Oct 12 18:58:20 2012 +0200
    24.3 @@ -8,7 +8,7 @@
    24.4  
    24.5  subsection {* Type definition and primitive operations *}
    24.6  
    24.7 -typedef (open) ('a, 'b) mapping = "UNIV :: ('a \<rightharpoonup> 'b) set"
    24.8 +typedef ('a, 'b) mapping = "UNIV :: ('a \<rightharpoonup> 'b) set"
    24.9    morphisms lookup Mapping ..
   24.10  
   24.11  lemma lookup_Mapping [simp]:
    25.1 --- a/src/HOL/Library/Multiset.thy	Fri Oct 12 15:08:29 2012 +0200
    25.2 +++ b/src/HOL/Library/Multiset.thy	Fri Oct 12 18:58:20 2012 +0200
    25.3 @@ -12,7 +12,7 @@
    25.4  
    25.5  definition "multiset = {f :: 'a => nat. finite {x. f x > 0}}"
    25.6  
    25.7 -typedef (open) 'a multiset = "multiset :: ('a => nat) set"
    25.8 +typedef 'a multiset = "multiset :: ('a => nat) set"
    25.9    morphisms count Abs_multiset
   25.10    unfolding multiset_def
   25.11  proof
    26.1 --- a/src/HOL/Library/Numeral_Type.thy	Fri Oct 12 15:08:29 2012 +0200
    26.2 +++ b/src/HOL/Library/Numeral_Type.thy	Fri Oct 12 18:58:20 2012 +0200
    26.3 @@ -10,16 +10,16 @@
    26.4  
    26.5  subsection {* Numeral Types *}
    26.6  
    26.7 -typedef (open) num0 = "UNIV :: nat set" ..
    26.8 -typedef (open) num1 = "UNIV :: unit set" ..
    26.9 +typedef num0 = "UNIV :: nat set" ..
   26.10 +typedef num1 = "UNIV :: unit set" ..
   26.11  
   26.12 -typedef (open) 'a bit0 = "{0 ..< 2 * int CARD('a::finite)}"
   26.13 +typedef 'a bit0 = "{0 ..< 2 * int CARD('a::finite)}"
   26.14  proof
   26.15    show "0 \<in> {0 ..< 2 * int CARD('a)}"
   26.16      by simp
   26.17  qed
   26.18  
   26.19 -typedef (open) 'a bit1 = "{0 ..< 1 + 2 * int CARD('a::finite)}"
   26.20 +typedef 'a bit1 = "{0 ..< 1 + 2 * int CARD('a::finite)}"
   26.21  proof
   26.22    show "0 \<in> {0 ..< 1 + 2 * int CARD('a)}"
   26.23      by simp
    27.1 --- a/src/HOL/Library/Polynomial.thy	Fri Oct 12 15:08:29 2012 +0200
    27.2 +++ b/src/HOL/Library/Polynomial.thy	Fri Oct 12 18:58:20 2012 +0200
    27.3 @@ -13,7 +13,7 @@
    27.4  
    27.5  definition "Poly = {f::nat \<Rightarrow> 'a::zero. \<exists>n. \<forall>i>n. f i = 0}"
    27.6  
    27.7 -typedef (open) 'a poly = "Poly :: (nat => 'a::zero) set"
    27.8 +typedef 'a poly = "Poly :: (nat => 'a::zero) set"
    27.9    morphisms coeff Abs_poly
   27.10    unfolding Poly_def by auto
   27.11  
    28.1 --- a/src/HOL/Library/Quotient_Type.thy	Fri Oct 12 15:08:29 2012 +0200
    28.2 +++ b/src/HOL/Library/Quotient_Type.thy	Fri Oct 12 18:58:20 2012 +0200
    28.3 @@ -60,7 +60,7 @@
    28.4  
    28.5  definition "quot = {{x. a \<sim> x} | a::'a::eqv. True}"
    28.6  
    28.7 -typedef (open) 'a quot = "quot :: 'a::eqv set set"
    28.8 +typedef 'a quot = "quot :: 'a::eqv set set"
    28.9    unfolding quot_def by blast
   28.10  
   28.11  lemma quotI [intro]: "{x. a \<sim> x} \<in> quot"
    29.1 --- a/src/HOL/Library/RBT.thy	Fri Oct 12 15:08:29 2012 +0200
    29.2 +++ b/src/HOL/Library/RBT.thy	Fri Oct 12 18:58:20 2012 +0200
    29.3 @@ -10,7 +10,7 @@
    29.4  
    29.5  subsection {* Type definition *}
    29.6  
    29.7 -typedef (open) ('a, 'b) rbt = "{t :: ('a\<Colon>linorder, 'b) RBT_Impl.rbt. is_rbt t}"
    29.8 +typedef ('a, 'b) rbt = "{t :: ('a\<Colon>linorder, 'b) RBT_Impl.rbt. is_rbt t}"
    29.9    morphisms impl_of RBT
   29.10  proof -
   29.11    have "RBT_Impl.Empty \<in> ?rbt" by simp
    30.1 --- a/src/HOL/Library/Saturated.thy	Fri Oct 12 15:08:29 2012 +0200
    30.2 +++ b/src/HOL/Library/Saturated.thy	Fri Oct 12 18:58:20 2012 +0200
    30.3 @@ -12,7 +12,7 @@
    30.4  
    30.5  subsection {* The type of saturated naturals *}
    30.6  
    30.7 -typedef (open) ('a::len) sat = "{.. len_of TYPE('a)}"
    30.8 +typedef ('a::len) sat = "{.. len_of TYPE('a)}"
    30.9    morphisms nat_of Abs_sat
   30.10    by auto
   30.11  
    31.1 --- a/src/HOL/Library/Target_Numeral.thy	Fri Oct 12 15:08:29 2012 +0200
    31.2 +++ b/src/HOL/Library/Target_Numeral.thy	Fri Oct 12 18:58:20 2012 +0200
    31.3 @@ -4,7 +4,7 @@
    31.4  
    31.5  subsection {* Type of target language numerals *}
    31.6  
    31.7 -typedef (open) int = "UNIV \<Colon> int set"
    31.8 +typedef int = "UNIV \<Colon> int set"
    31.9    morphisms int_of of_int ..
   31.10  
   31.11  hide_type (open) int
    32.1 --- a/src/HOL/Limits.thy	Fri Oct 12 15:08:29 2012 +0200
    32.2 +++ b/src/HOL/Limits.thy	Fri Oct 12 18:58:20 2012 +0200
    32.3 @@ -20,7 +20,7 @@
    32.4    assumes conj: "F (\<lambda>x. P x) \<Longrightarrow> F (\<lambda>x. Q x) \<Longrightarrow> F (\<lambda>x. P x \<and> Q x)"
    32.5    assumes mono: "\<forall>x. P x \<longrightarrow> Q x \<Longrightarrow> F (\<lambda>x. P x) \<Longrightarrow> F (\<lambda>x. Q x)"
    32.6  
    32.7 -typedef (open) 'a filter = "{F :: ('a \<Rightarrow> bool) \<Rightarrow> bool. is_filter F}"
    32.8 +typedef 'a filter = "{F :: ('a \<Rightarrow> bool) \<Rightarrow> bool. is_filter F}"
    32.9  proof
   32.10    show "(\<lambda>x. True) \<in> ?filter" by (auto intro: is_filter.intro)
   32.11  qed
    33.1 --- a/src/HOL/Matrix_LP/Matrix.thy	Fri Oct 12 15:08:29 2012 +0200
    33.2 +++ b/src/HOL/Matrix_LP/Matrix.thy	Fri Oct 12 18:58:20 2012 +0200
    33.3 @@ -13,7 +13,7 @@
    33.4  
    33.5  definition "matrix = {(f::(nat \<Rightarrow> nat \<Rightarrow> 'a::zero)). finite (nonzero_positions f)}"
    33.6  
    33.7 -typedef (open) 'a matrix = "matrix :: (nat \<Rightarrow> nat \<Rightarrow> 'a::zero) set"
    33.8 +typedef 'a matrix = "matrix :: (nat \<Rightarrow> nat \<Rightarrow> 'a::zero) set"
    33.9    unfolding matrix_def
   33.10  proof
   33.11    show "(\<lambda>j i. 0) \<in> {(f::(nat \<Rightarrow> nat \<Rightarrow> 'a::zero)). finite (nonzero_positions f)}"
    34.1 --- a/src/HOL/Multivariate_Analysis/Finite_Cartesian_Product.thy	Fri Oct 12 15:08:29 2012 +0200
    34.2 +++ b/src/HOL/Multivariate_Analysis/Finite_Cartesian_Product.thy	Fri Oct 12 18:58:20 2012 +0200
    34.3 @@ -13,7 +13,7 @@
    34.4  
    34.5  subsection {* Finite Cartesian products, with indexing and lambdas. *}
    34.6  
    34.7 -typedef (open) ('a, 'b) vec = "UNIV :: (('b::finite) \<Rightarrow> 'a) set"
    34.8 +typedef ('a, 'b) vec = "UNIV :: (('b::finite) \<Rightarrow> 'a) set"
    34.9    morphisms vec_nth vec_lambda ..
   34.10  
   34.11  notation
    35.1 --- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Fri Oct 12 15:08:29 2012 +0200
    35.2 +++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Fri Oct 12 18:58:20 2012 +0200
    35.3 @@ -13,7 +13,7 @@
    35.4  subsection {* General notion of a topology as a value *}
    35.5  
    35.6  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))"
    35.7 -typedef (open) 'a topology = "{L::('a set) \<Rightarrow> bool. istopology L}"
    35.8 +typedef 'a topology = "{L::('a set) \<Rightarrow> bool. istopology L}"
    35.9    morphisms "openin" "topology"
   35.10    unfolding istopology_def by blast
   35.11  
    36.1 --- a/src/HOL/NSA/StarDef.thy	Fri Oct 12 15:08:29 2012 +0200
    36.2 +++ b/src/HOL/NSA/StarDef.thy	Fri Oct 12 18:58:20 2012 +0200
    36.3 @@ -40,7 +40,7 @@
    36.4  
    36.5  definition "star = (UNIV :: (nat \<Rightarrow> 'a) set) // starrel"
    36.6  
    36.7 -typedef (open) 'a star = "star :: (nat \<Rightarrow> 'a) set set"
    36.8 +typedef 'a star = "star :: (nat \<Rightarrow> 'a) set set"
    36.9    unfolding star_def by (auto intro: quotientI)
   36.10  
   36.11  definition
    37.1 --- a/src/HOL/Nat.thy	Fri Oct 12 15:08:29 2012 +0200
    37.2 +++ b/src/HOL/Nat.thy	Fri Oct 12 18:58:20 2012 +0200
    37.3 @@ -33,7 +33,7 @@
    37.4    Zero_RepI: "Nat Zero_Rep"
    37.5  | Suc_RepI: "Nat i \<Longrightarrow> Nat (Suc_Rep i)"
    37.6  
    37.7 -typedef (open) nat = "{n. Nat n}"
    37.8 +typedef nat = "{n. Nat n}"
    37.9    morphisms Rep_Nat Abs_Nat
   37.10    using Nat.Zero_RepI by auto
   37.11  
    38.1 --- a/src/HOL/Nitpick_Examples/Manual_Nits.thy	Fri Oct 12 15:08:29 2012 +0200
    38.2 +++ b/src/HOL/Nitpick_Examples/Manual_Nits.thy	Fri Oct 12 18:58:20 2012 +0200
    38.3 @@ -95,7 +95,7 @@
    38.4  subsection {* 2.7. Typedefs, Records, Rationals, and Reals *}
    38.5  
    38.6  definition "three = {0\<Colon>nat, 1, 2}"
    38.7 -typedef (open) three = three
    38.8 +typedef three = three
    38.9    unfolding three_def by blast
   38.10  
   38.11  definition A :: three where "A \<equiv> Abs_three 0"
   38.12 @@ -201,7 +201,7 @@
   38.13  (* BEGIN LAZY LIST SETUP *)
   38.14  definition "llist = (UNIV\<Colon>('a list + (nat \<Rightarrow> 'a)) set)"
   38.15  
   38.16 -typedef (open) 'a llist = "llist\<Colon>('a list + (nat \<Rightarrow> 'a)) set"
   38.17 +typedef 'a llist = "llist\<Colon>('a list + (nat \<Rightarrow> 'a)) set"
   38.18  unfolding llist_def by auto
   38.19  
   38.20  definition LNil where
    39.1 --- a/src/HOL/Nitpick_Examples/Refute_Nits.thy	Fri Oct 12 15:08:29 2012 +0200
    39.2 +++ b/src/HOL/Nitpick_Examples/Refute_Nits.thy	Fri Oct 12 18:58:20 2012 +0200
    39.3 @@ -541,7 +541,7 @@
    39.4  
    39.5  definition "myTdef = insert (undefined::'a) (undefined::'a set)"
    39.6  
    39.7 -typedef (open) 'a myTdef = "myTdef :: 'a set"
    39.8 +typedef 'a myTdef = "myTdef :: 'a set"
    39.9  unfolding myTdef_def by auto
   39.10  
   39.11  lemma "(x\<Colon>'a myTdef) = y"
   39.12 @@ -552,7 +552,7 @@
   39.13  
   39.14  definition "T_bij = {(f::'a\<Rightarrow>'a). \<forall>y. \<exists>!x. f x = y}"
   39.15  
   39.16 -typedef (open) 'a T_bij = "T_bij :: ('a \<Rightarrow> 'a) set"
   39.17 +typedef 'a T_bij = "T_bij :: ('a \<Rightarrow> 'a) set"
   39.18  unfolding T_bij_def by auto
   39.19  
   39.20  lemma "P (f\<Colon>(myTdecl myTdef) T_bij)"
    40.1 --- a/src/HOL/Nitpick_Examples/Typedef_Nits.thy	Fri Oct 12 15:08:29 2012 +0200
    40.2 +++ b/src/HOL/Nitpick_Examples/Typedef_Nits.thy	Fri Oct 12 18:58:20 2012 +0200
    40.3 @@ -15,7 +15,7 @@
    40.4                  timeout = 240]
    40.5  
    40.6  definition "three = {0\<Colon>nat, 1, 2}"
    40.7 -typedef (open) three = three
    40.8 +typedef three = three
    40.9  unfolding three_def by blast
   40.10  
   40.11  definition A :: three where "A \<equiv> Abs_three 0"
   40.12 @@ -28,7 +28,7 @@
   40.13  
   40.14  definition "one_or_two = {undefined False\<Colon>'a, undefined True}"
   40.15  
   40.16 -typedef (open) 'a one_or_two = "one_or_two :: 'a set"
   40.17 +typedef 'a one_or_two = "one_or_two :: 'a set"
   40.18  unfolding one_or_two_def by auto
   40.19  
   40.20  lemma "x = (y\<Colon>unit one_or_two)"
   40.21 @@ -54,7 +54,7 @@
   40.22  
   40.23  definition "bounded = {n\<Colon>nat. finite (UNIV \<Colon> 'a set) \<longrightarrow> n < card (UNIV \<Colon> 'a set)}"
   40.24  
   40.25 -typedef (open) 'a bounded = "bounded(TYPE('a))"
   40.26 +typedef 'a bounded = "bounded(TYPE('a))"
   40.27  unfolding bounded_def
   40.28  apply (rule_tac x = 0 in exI)
   40.29  apply (case_tac "card UNIV = 0")
    41.1 --- a/src/HOL/Nominal/Nominal.thy	Fri Oct 12 15:08:29 2012 +0200
    41.2 +++ b/src/HOL/Nominal/Nominal.thy	Fri Oct 12 18:58:20 2012 +0200
    41.3 @@ -3376,7 +3376,7 @@
    41.4  
    41.5  definition "ABS = ABS_set"
    41.6  
    41.7 -typedef (open) ('x,'a) ABS ("\<guillemotleft>_\<guillemotright>_" [1000,1000] 1000) =
    41.8 +typedef ('x,'a) ABS ("\<guillemotleft>_\<guillemotright>_" [1000,1000] 1000) =
    41.9      "ABS::('x\<Rightarrow>('a noption)) set"
   41.10    morphisms Rep_ABS Abs_ABS
   41.11    unfolding ABS_def
    42.1 --- a/src/HOL/Probability/Sigma_Algebra.thy	Fri Oct 12 15:08:29 2012 +0200
    42.2 +++ b/src/HOL/Probability/Sigma_Algebra.thy	Fri Oct 12 18:58:20 2012 +0200
    42.3 @@ -997,7 +997,7 @@
    42.4  definition measure_space :: "'a set \<Rightarrow> 'a set set \<Rightarrow> ('a set \<Rightarrow> ereal) \<Rightarrow> bool" where
    42.5    "measure_space \<Omega> A \<mu> \<longleftrightarrow> sigma_algebra \<Omega> A \<and> positive A \<mu> \<and> countably_additive A \<mu>"
    42.6  
    42.7 -typedef (open) 'a measure = "{(\<Omega>::'a set, A, \<mu>). (\<forall>a\<in>-A. \<mu> a = 0) \<and> measure_space \<Omega> A \<mu> }"
    42.8 +typedef 'a measure = "{(\<Omega>::'a set, A, \<mu>). (\<forall>a\<in>-A. \<mu> a = 0) \<and> measure_space \<Omega> A \<mu> }"
    42.9  proof
   42.10    have "sigma_algebra UNIV {{}, UNIV}"
   42.11      by (auto simp: sigma_algebra_iff2)
    43.1 --- a/src/HOL/Product_Type.thy	Fri Oct 12 15:08:29 2012 +0200
    43.2 +++ b/src/HOL/Product_Type.thy	Fri Oct 12 18:58:20 2012 +0200
    43.3 @@ -43,7 +43,7 @@
    43.4  
    43.5  subsection {* The @{text unit} type *}
    43.6  
    43.7 -typedef (open) unit = "{True}"
    43.8 +typedef unit = "{True}"
    43.9    by auto
   43.10  
   43.11  definition Unity :: unit  ("'(')")
   43.12 @@ -132,7 +132,7 @@
   43.13  
   43.14  definition "prod = {f. \<exists>a b. f = Pair_Rep (a\<Colon>'a) (b\<Colon>'b)}"
   43.15  
   43.16 -typedef (open) ('a, 'b) prod (infixr "*" 20) = "prod :: ('a \<Rightarrow> 'b \<Rightarrow> bool) set"
   43.17 +typedef ('a, 'b) prod (infixr "*" 20) = "prod :: ('a \<Rightarrow> 'b \<Rightarrow> bool) set"
   43.18    unfolding prod_def by auto
   43.19  
   43.20  type_notation (xsymbols)
    44.1 --- a/src/HOL/Quickcheck_Narrowing.thy	Fri Oct 12 15:08:29 2012 +0200
    44.2 +++ b/src/HOL/Quickcheck_Narrowing.thy	Fri Oct 12 18:58:20 2012 +0200
    44.3 @@ -25,7 +25,7 @@
    44.4  
    44.5  subsubsection {* Type @{text "code_int"} for Haskell Quickcheck's Int type *}
    44.6  
    44.7 -typedef (open) code_int = "UNIV \<Colon> int set"
    44.8 +typedef code_int = "UNIV \<Colon> int set"
    44.9    morphisms int_of of_int by rule
   44.10  
   44.11  lemma of_int_int_of [simp]:
    45.1 --- a/src/HOL/Quotient_Examples/Lift_DList.thy	Fri Oct 12 15:08:29 2012 +0200
    45.2 +++ b/src/HOL/Quotient_Examples/Lift_DList.thy	Fri Oct 12 18:58:20 2012 +0200
    45.3 @@ -8,7 +8,7 @@
    45.4  
    45.5  subsection {* The type of distinct lists *}
    45.6  
    45.7 -typedef (open) 'a dlist = "{xs::'a list. distinct xs}"
    45.8 +typedef 'a dlist = "{xs::'a list. distinct xs}"
    45.9    morphisms list_of_dlist Abs_dlist
   45.10  proof
   45.11    show "[] \<in> {xs. distinct xs}" by simp
    46.1 --- a/src/HOL/Quotient_Examples/Lift_Set.thy	Fri Oct 12 15:08:29 2012 +0200
    46.2 +++ b/src/HOL/Quotient_Examples/Lift_Set.thy	Fri Oct 12 18:58:20 2012 +0200
    46.3 @@ -10,7 +10,7 @@
    46.4  
    46.5  definition set where "set = (UNIV :: ('a \<Rightarrow> bool) set)"
    46.6  
    46.7 -typedef (open) 'a set = "set :: ('a \<Rightarrow> bool) set"
    46.8 +typedef 'a set = "set :: ('a \<Rightarrow> bool) set"
    46.9    morphisms member Set
   46.10    unfolding set_def by auto
   46.11  
    47.1 --- a/src/HOL/SMT_Examples/SMT_Tests.thy	Fri Oct 12 15:08:29 2012 +0200
    47.2 +++ b/src/HOL/SMT_Examples/SMT_Tests.thy	Fri Oct 12 18:58:20 2012 +0200
    47.3 @@ -760,7 +760,7 @@
    47.4  
    47.5  definition "three = {1, 2, 3::int}"
    47.6  
    47.7 -typedef (open) three = three
    47.8 +typedef three = three
    47.9    unfolding three_def by auto
   47.10  
   47.11  definition n1 where "n1 = Abs_three 1"
    48.1 --- a/src/HOL/String.thy	Fri Oct 12 15:08:29 2012 +0200
    48.2 +++ b/src/HOL/String.thy	Fri Oct 12 18:58:20 2012 +0200
    48.3 @@ -152,7 +152,7 @@
    48.4  
    48.5  subsection {* Strings as dedicated type *}
    48.6  
    48.7 -typedef (open) literal = "UNIV :: string set"
    48.8 +typedef literal = "UNIV :: string set"
    48.9    morphisms explode STR ..
   48.10  
   48.11  instantiation literal :: size
    49.1 --- a/src/HOL/Sum_Type.thy	Fri Oct 12 15:08:29 2012 +0200
    49.2 +++ b/src/HOL/Sum_Type.thy	Fri Oct 12 18:58:20 2012 +0200
    49.3 @@ -19,7 +19,7 @@
    49.4  
    49.5  definition "sum = {f. (\<exists>a. f = Inl_Rep (a::'a)) \<or> (\<exists>b. f = Inr_Rep (b::'b))}"
    49.6  
    49.7 -typedef (open) ('a, 'b) sum (infixr "+" 10) = "sum :: ('a => 'b => bool => bool) set"
    49.8 +typedef ('a, 'b) sum (infixr "+" 10) = "sum :: ('a => 'b => bool => bool) set"
    49.9    unfolding sum_def by auto
   49.10  
   49.11  lemma Inl_RepI: "Inl_Rep a \<in> sum"
    50.1 --- a/src/HOL/Tools/typedef.ML	Fri Oct 12 15:08:29 2012 +0200
    50.2 +++ b/src/HOL/Tools/typedef.ML	Fri Oct 12 18:58:20 2012 +0200
    50.3 @@ -276,17 +276,12 @@
    50.4  val _ =
    50.5    Outer_Syntax.local_theory_to_proof @{command_spec "typedef"}
    50.6      "HOL type definition (requires non-emptiness proof)"
    50.7 -    (Scan.optional (@{keyword "("} |--
    50.8 -        ((@{keyword "open"} >> K false) -- Scan.option Parse.binding ||
    50.9 -          Parse.binding >> (fn s => (true, SOME s))) --| @{keyword ")"}) (true, NONE) --
   50.10 +    (Scan.option (@{keyword "("} |-- Parse.binding --| @{keyword ")"}) --
   50.11        (Parse.type_args_constrained -- Parse.binding) --
   50.12          Parse.opt_mixfix -- (@{keyword "="} |-- Parse.term) --
   50.13          Scan.option (@{keyword "morphisms"} |-- Parse.!!! (Parse.binding -- Parse.binding))
   50.14 -    >> (fn ((((((def, opt_name), (args, t)), mx), A), morphs)) => fn lthy =>
   50.15 -          (if def then
   50.16 -            error "typedef with implicit set definition -- use \"typedef (open)\" instead"
   50.17 -           else ();
   50.18 -           typedef_cmd (the_default t opt_name, (t, args, mx), A, morphs) lthy)));
   50.19 +    >> (fn (((((opt_name, (args, t)), mx), A), morphs)) => fn lthy =>
   50.20 +           typedef_cmd (the_default t opt_name, (t, args, mx), A, morphs) lthy));
   50.21  
   50.22  end;
   50.23  
    51.1 --- a/src/HOL/UNITY/UNITY.thy	Fri Oct 12 15:08:29 2012 +0200
    51.2 +++ b/src/HOL/UNITY/UNITY.thy	Fri Oct 12 18:58:20 2012 +0200
    51.3 @@ -17,7 +17,7 @@
    51.4      {(init:: 'a set, acts :: ('a * 'a)set set,
    51.5        allowed :: ('a * 'a)set set). Id \<in> acts & Id: allowed}"
    51.6  
    51.7 -typedef (open) 'a program = "Program :: ('a set * ('a * 'a) set set * ('a * 'a) set set) set"
    51.8 +typedef 'a program = "Program :: ('a set * ('a * 'a) set set * ('a * 'a) set set) set"
    51.9    morphisms Rep_Program Abs_Program
   51.10    unfolding Program_def by blast
   51.11  
    52.1 --- a/src/HOL/Word/Word.thy	Fri Oct 12 15:08:29 2012 +0200
    52.2 +++ b/src/HOL/Word/Word.thy	Fri Oct 12 18:58:20 2012 +0200
    52.3 @@ -16,7 +16,7 @@
    52.4  
    52.5  subsection {* Type definition *}
    52.6  
    52.7 -typedef (open) 'a word = "{(0::int) ..< 2^len_of TYPE('a::len0)}"
    52.8 +typedef 'a word = "{(0::int) ..< 2^len_of TYPE('a::len0)}"
    52.9    morphisms uint Abs_word by auto
   52.10  
   52.11  lemma uint_nonnegative:
    53.1 --- a/src/HOL/ZF/Games.thy	Fri Oct 12 15:08:29 2012 +0200
    53.2 +++ b/src/HOL/ZF/Games.thy	Fri Oct 12 18:58:20 2012 +0200
    53.3 @@ -191,7 +191,7 @@
    53.4  
    53.5  definition "game = games_lfp"
    53.6  
    53.7 -typedef (open) game = game
    53.8 +typedef game = game
    53.9    unfolding game_def by (blast intro: games_lfp_nonempty)
   53.10  
   53.11  definition left_options :: "game \<Rightarrow> game zet" where
   53.12 @@ -843,7 +843,7 @@
   53.13  
   53.14  definition "Pg = UNIV//eq_game_rel"
   53.15  
   53.16 -typedef (open) Pg = Pg
   53.17 +typedef Pg = Pg
   53.18    unfolding Pg_def by (auto simp add: quotient_def)
   53.19  
   53.20  lemma equiv_eq_game[simp]: "equiv UNIV eq_game_rel"
    54.1 --- a/src/HOL/ZF/Zet.thy	Fri Oct 12 15:08:29 2012 +0200
    54.2 +++ b/src/HOL/ZF/Zet.thy	Fri Oct 12 18:58:20 2012 +0200
    54.3 @@ -11,7 +11,7 @@
    54.4  
    54.5  definition "zet = {A :: 'a set | A f z. inj_on f A \<and> f ` A \<subseteq> explode z}"
    54.6  
    54.7 -typedef (open) 'a zet = "zet :: 'a set set"
    54.8 +typedef 'a zet = "zet :: 'a set set"
    54.9    unfolding zet_def by blast
   54.10  
   54.11  definition zin :: "'a \<Rightarrow> 'a zet \<Rightarrow> bool" where
    55.1 --- a/src/HOL/ex/Dedekind_Real.thy	Fri Oct 12 15:08:29 2012 +0200
    55.2 +++ b/src/HOL/ex/Dedekind_Real.thy	Fri Oct 12 18:58:20 2012 +0200
    55.3 @@ -46,7 +46,7 @@
    55.4  
    55.5  definition "preal = {A. cut A}"
    55.6  
    55.7 -typedef (open) preal = preal
    55.8 +typedef preal = preal
    55.9    unfolding preal_def by (blast intro: cut_of_rat [OF zero_less_one])
   55.10  
   55.11  definition
   55.12 @@ -1171,7 +1171,7 @@
   55.13  
   55.14  definition "Real = UNIV//realrel"
   55.15  
   55.16 -typedef (open) real = Real
   55.17 +typedef real = Real
   55.18    morphisms Rep_Real Abs_Real
   55.19    unfolding Real_def by (auto simp add: quotient_def)
   55.20  
    56.1 --- a/src/HOL/ex/Executable_Relation.thy	Fri Oct 12 15:08:29 2012 +0200
    56.2 +++ b/src/HOL/ex/Executable_Relation.thy	Fri Oct 12 18:58:20 2012 +0200
    56.3 @@ -6,7 +6,7 @@
    56.4  
    56.5  subsubsection {* Definition of the dedicated type for relations *}
    56.6  
    56.7 -typedef (open) 'a rel = "UNIV :: (('a * 'a) set) set"
    56.8 +typedef 'a rel = "UNIV :: (('a * 'a) set) set"
    56.9  morphisms set_of_rel rel_of_set by simp
   56.10  
   56.11  setup_lifting type_definition_rel
    57.1 --- a/src/HOL/ex/PER.thy	Fri Oct 12 15:08:29 2012 +0200
    57.2 +++ b/src/HOL/ex/PER.thy	Fri Oct 12 18:58:20 2012 +0200
    57.3 @@ -153,7 +153,7 @@
    57.4  
    57.5  definition "quot = {{x. a \<sim> x}| a::'a::partial_equiv. True}"
    57.6  
    57.7 -typedef (open) 'a quot = "quot :: 'a::partial_equiv set set"
    57.8 +typedef 'a quot = "quot :: 'a::partial_equiv set set"
    57.9    unfolding quot_def by blast
   57.10  
   57.11  lemma quotI [intro]: "{x. a \<sim> x} \<in> quot"
    58.1 --- a/src/HOL/ex/Refute_Examples.thy	Fri Oct 12 15:08:29 2012 +0200
    58.2 +++ b/src/HOL/ex/Refute_Examples.thy	Fri Oct 12 18:58:20 2012 +0200
    58.3 @@ -485,7 +485,7 @@
    58.4  
    58.5  definition "myTdef = insert (undefined::'a) (undefined::'a set)"
    58.6  
    58.7 -typedef (open) 'a myTdef = "myTdef :: 'a set"
    58.8 +typedef 'a myTdef = "myTdef :: 'a set"
    58.9    unfolding myTdef_def by auto
   58.10  
   58.11  lemma "(x::'a myTdef) = y"
   58.12 @@ -496,7 +496,7 @@
   58.13  
   58.14  definition "T_bij = {(f::'a\<Rightarrow>'a). \<forall>y. \<exists>!x. f x = y}"
   58.15  
   58.16 -typedef (open) 'a T_bij = "T_bij :: ('a \<Rightarrow> 'a) set"
   58.17 +typedef 'a T_bij = "T_bij :: ('a \<Rightarrow> 'a) set"
   58.18    unfolding T_bij_def by auto
   58.19  
   58.20  lemma "P (f::(myTdecl myTdef) T_bij)"