# HG changeset patch
# User wenzelm
# Date 1322666830 -3600
# Node ID 4a87436182570369604aa86ee28243f200806d42
# Parent  bbd2c7ffc02c28ec14841ecaea510709167cbd7f
prefer typedef without extra definition and alternative name;
tuned proofs;

diff -r bbd2c7ffc02c -r 4a8743618257 src/HOL/Algebra/poly/UnivPoly2.thy
--- a/src/HOL/Algebra/poly/UnivPoly2.thy	Wed Nov 30 16:05:15 2011 +0100
+++ b/src/HOL/Algebra/poly/UnivPoly2.thy	Wed Nov 30 16:27:10 2011 +0100
@@ -39,9 +39,15 @@
   with nonzero show ?thesis by contradiction
 qed
 
-typedef (UP)
-    ('a) up = "{f :: nat => 'a::zero. EX n. bound n f}"
-  by (rule+)   (* Question: what does trace_rule show??? *)
+
+definition "UP = {f :: nat => 'a::zero. EX n. bound n f}"
+
+typedef (open) 'a up = "UP :: (nat => 'a::zero) set"
+  morphisms Rep_UP Abs_UP
+proof -
+  have "bound 0 (\<lambda>_. 0::'a)" by (rule boundI) (rule refl)
+  then show ?thesis unfolding UP_def by blast
+qed
 
 
 section {* Constants *}
diff -r bbd2c7ffc02c -r 4a8743618257 src/HOL/Code_Numeral.thy
--- a/src/HOL/Code_Numeral.thy	Wed Nov 30 16:05:15 2011 +0100
+++ b/src/HOL/Code_Numeral.thy	Wed Nov 30 16:27:10 2011 +0100
@@ -14,7 +14,7 @@
 subsection {* Datatype of target language numerals *}
 
 typedef (open) code_numeral = "UNIV \<Colon> nat set"
-  morphisms nat_of of_nat by rule
+  morphisms nat_of of_nat ..
 
 lemma of_nat_nat_of [simp]:
   "of_nat (nat_of k) = k"
diff -r bbd2c7ffc02c -r 4a8743618257 src/HOL/Datatype.thy
--- a/src/HOL/Datatype.thy	Wed Nov 30 16:05:15 2011 +0100
+++ b/src/HOL/Datatype.thy	Wed Nov 30 16:27:10 2011 +0100
@@ -21,10 +21,11 @@
 
 subsection {* The datatype universe *}
 
-typedef (Node)
-  ('a,'b) node = "{p. EX f x k. p = (f::nat=>'b+nat, x::'a+nat) & f k = Inr 0}"
-    --{*it is a subtype of @{text "(nat=>'b+nat) * ('a+nat)"}*}
-  by auto
+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"
+  morphisms Rep_Node Abs_Node
+  unfolding Node_def by auto
 
 text{*Datatypes will be represented by sets of type @{text node}*}
 
diff -r bbd2c7ffc02c -r 4a8743618257 src/HOL/HOLCF/Compact_Basis.thy
--- a/src/HOL/HOLCF/Compact_Basis.thy	Wed Nov 30 16:05:15 2011 +0100
+++ b/src/HOL/HOLCF/Compact_Basis.thy	Wed Nov 30 16:27:10 2011 +0100
@@ -12,9 +12,13 @@
 
 subsection {* A compact basis for powerdomains *}
 
-typedef 'a pd_basis =
-  "{S::'a compact_basis set. finite S \<and> S \<noteq> {}}"
-by (rule_tac x="{arbitrary}" in exI, simp)
+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"
+  unfolding pd_basis_def
+  apply (rule_tac x="{arbitrary}" in exI)
+  apply simp
+  done
 
 lemma finite_Rep_pd_basis [simp]: "finite (Rep_pd_basis u)"
 by (insert Rep_pd_basis [of u, unfolded pd_basis_def]) simp
diff -r bbd2c7ffc02c -r 4a8743618257 src/HOL/Induct/QuoDataType.thy
--- a/src/HOL/Induct/QuoDataType.thy	Wed Nov 30 16:05:15 2011 +0100
+++ b/src/HOL/Induct/QuoDataType.thy	Wed Nov 30 16:27:10 2011 +0100
@@ -123,8 +123,11 @@
 
 subsection{*The Initial Algebra: A Quotiented Message Type*}
 
-typedef (Msg)  msg = "UNIV//msgrel"
-  by (auto simp add: quotient_def)
+definition "Msg = UNIV//msgrel"
+
+typedef (open) msg = Msg
+  morphisms Rep_Msg Abs_Msg
+  unfolding Msg_def by (auto simp add: quotient_def)
 
 
 text{*The abstract message constructors*}
diff -r bbd2c7ffc02c -r 4a8743618257 src/HOL/Induct/QuoNestedDataType.thy
--- a/src/HOL/Induct/QuoNestedDataType.thy	Wed Nov 30 16:05:15 2011 +0100
+++ b/src/HOL/Induct/QuoNestedDataType.thy	Wed Nov 30 16:27:10 2011 +0100
@@ -142,9 +142,11 @@
 
 subsection{*The Initial Algebra: A Quotiented Message Type*}
 
+definition "Exp = UNIV//exprel"
 
-typedef (Exp)  exp = "UNIV//exprel"
-    by (auto simp add: quotient_def)
+typedef (open) exp = Exp
+  morphisms Rep_Exp Abs_Exp
+  unfolding Exp_def by (auto simp add: quotient_def)
 
 text{*The abstract message constructors*}
 
diff -r bbd2c7ffc02c -r 4a8743618257 src/HOL/Induct/SList.thy
--- a/src/HOL/Induct/SList.thy	Wed Nov 30 16:05:15 2011 +0100
+++ b/src/HOL/Induct/SList.thy	Wed Nov 30 16:27:10 2011 +0100
@@ -53,9 +53,11 @@
   | CONS_I: "[| a: A;  M: list A |] ==> CONS a M : list A"
 
 
-typedef (List)
-    'a list = "list(range Leaf) :: 'a item set" 
-  by (blast intro: list.NIL_I)
+definition "List = list (range Leaf)"
+
+typedef (open) 'a list = "List :: 'a item set"
+  morphisms Rep_List Abs_List
+  unfolding List_def by (blast intro: list.NIL_I)
 
 abbreviation "Case == Datatype.Case"
 abbreviation "Split == Datatype.Split"
@@ -224,7 +226,7 @@
 lemmas Cons_inject2 = Cons_Cons_eq [THEN iffD1, THEN conjE]
 
 lemma CONS_D: "CONS M N: list(A) ==> M: A & N: list(A)"
-  by (induct L == "CONS M N" set: list) auto
+  by (induct L == "CONS M N" rule: list.induct) auto
 
 lemma sexp_CONS_D: "CONS M N: sexp ==> M: sexp & N: sexp"
 apply (simp add: CONS_def In1_def)
diff -r bbd2c7ffc02c -r 4a8743618257 src/HOL/Int.thy
--- a/src/HOL/Int.thy	Wed Nov 30 16:05:15 2011 +0100
+++ b/src/HOL/Int.thy	Wed Nov 30 16:27:10 2011 +0100
@@ -18,9 +18,11 @@
 definition intrel :: "((nat \<times> nat) \<times> (nat \<times> nat)) set" where
   "intrel = {((x, y), (u, v)) | x y u v. x + v = u +y }"
 
-typedef (Integ)
-  int = "UNIV//intrel"
-  by (auto simp add: quotient_def)
+definition "Integ = UNIV//intrel"
+
+typedef (open) int = Integ
+  morphisms Rep_Integ Abs_Integ
+  unfolding Integ_def by (auto simp add: quotient_def)
 
 instantiation int :: "{zero, one, plus, minus, uminus, times, ord, abs, sgn}"
 begin
diff -r bbd2c7ffc02c -r 4a8743618257 src/HOL/Library/Dlist.thy
--- a/src/HOL/Library/Dlist.thy	Wed Nov 30 16:05:15 2011 +0100
+++ b/src/HOL/Library/Dlist.thy	Wed Nov 30 16:27:10 2011 +0100
@@ -11,7 +11,7 @@
 typedef (open) 'a dlist = "{xs::'a list. distinct xs}"
   morphisms list_of_dlist Abs_dlist
 proof
-  show "[] \<in> ?dlist" by simp
+  show "[] \<in> {xs. distinct xs}" by simp
 qed
 
 lemma dlist_eq_iff:
diff -r bbd2c7ffc02c -r 4a8743618257 src/HOL/Library/Fraction_Field.thy
--- a/src/HOL/Library/Fraction_Field.thy	Wed Nov 30 16:05:15 2011 +0100
+++ b/src/HOL/Library/Fraction_Field.thy	Wed Nov 30 16:27:10 2011 +0100
@@ -53,7 +53,10 @@
   shows "fractrel `` {x} = fractrel `` {y} \<longleftrightarrow> (x, y) \<in> fractrel"
   by (rule eq_equiv_class_iff, rule equiv_fractrel) (auto simp add: assms)
 
-typedef 'a fract = "{(x::'a\<times>'a). snd x \<noteq> (0::'a::idom)} // fractrel"
+definition "fract = {(x::'a\<times>'a). snd x \<noteq> (0::'a::idom)} // fractrel"
+
+typedef (open) '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
   then show "fractrel `` {(0::'a, 1)} \<in> {x. snd x \<noteq> 0} // fractrel" by (rule quotientI)
diff -r bbd2c7ffc02c -r 4a8743618257 src/HOL/Library/Multiset.thy
--- a/src/HOL/Library/Multiset.thy	Wed Nov 30 16:05:15 2011 +0100
+++ b/src/HOL/Library/Multiset.thy	Wed Nov 30 16:27:10 2011 +0100
@@ -10,10 +10,13 @@
 
 subsection {* The type of multisets *}
 
-typedef 'a multiset = "{f :: 'a => nat. finite {x. f x > 0}}"
+definition "multiset = {f :: 'a => nat. finite {x. f x > 0}}"
+
+typedef (open) 'a multiset = "multiset :: ('a => nat) set"
   morphisms count Abs_multiset
+  unfolding multiset_def
 proof
-  show "(\<lambda>x. 0::nat) \<in> ?multiset" by simp
+  show "(\<lambda>x. 0::nat) \<in> {f. finite {x. f x > 0}}" by simp
 qed
 
 lemmas multiset_typedef = Abs_multiset_inverse count_inverse count
diff -r bbd2c7ffc02c -r 4a8743618257 src/HOL/Library/Polynomial.thy
--- a/src/HOL/Library/Polynomial.thy	Wed Nov 30 16:05:15 2011 +0100
+++ b/src/HOL/Library/Polynomial.thy	Wed Nov 30 16:27:10 2011 +0100
@@ -11,15 +11,17 @@
 
 subsection {* Definition of type @{text poly} *}
 
-typedef (Poly) 'a poly = "{f::nat \<Rightarrow> 'a::zero. \<exists>n. \<forall>i>n. f i = 0}"
+definition "Poly = {f::nat \<Rightarrow> 'a::zero. \<exists>n. \<forall>i>n. f i = 0}"
+
+typedef (open) 'a poly = "Poly :: (nat => 'a::zero) set"
   morphisms coeff Abs_poly
-  by auto
+  unfolding Poly_def by auto
 
 lemma expand_poly_eq: "p = q \<longleftrightarrow> (\<forall>n. coeff p n = coeff q n)"
-by (simp add: coeff_inject [symmetric] fun_eq_iff)
+  by (simp add: coeff_inject [symmetric] fun_eq_iff)
 
 lemma poly_ext: "(\<And>n. coeff p n = coeff q n) \<Longrightarrow> p = q"
-by (simp add: expand_poly_eq)
+  by (simp add: expand_poly_eq)
 
 
 subsection {* Degree of a polynomial *}
diff -r bbd2c7ffc02c -r 4a8743618257 src/HOL/Library/Quotient_Type.thy
--- a/src/HOL/Library/Quotient_Type.thy	Wed Nov 30 16:05:15 2011 +0100
+++ b/src/HOL/Library/Quotient_Type.thy	Wed Nov 30 16:27:10 2011 +0100
@@ -58,8 +58,10 @@
  \emph{equivalence classes} over elements of the base type @{typ 'a}.
 *}
 
-typedef 'a quot = "{{x. a \<sim> x} | a::'a::eqv. True}"
-  by blast
+definition "quot = {{x. a \<sim> x} | a::'a::eqv. True}"
+
+typedef (open) 'a quot = "quot :: 'a::eqv set set"
+  unfolding quot_def by blast
 
 lemma quotI [intro]: "{x. a \<sim> x} \<in> quot"
   unfolding quot_def by blast
diff -r bbd2c7ffc02c -r 4a8743618257 src/HOL/Library/RBT.thy
--- a/src/HOL/Library/RBT.thy	Wed Nov 30 16:05:15 2011 +0100
+++ b/src/HOL/Library/RBT.thy	Wed Nov 30 16:27:10 2011 +0100
@@ -11,9 +11,8 @@
 
 typedef (open) ('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
-  then show ?thesis ..
+proof
+  show "RBT_Impl.Empty \<in> {t. is_rbt t}" by simp
 qed
 
 lemma rbt_eq_iff:
diff -r bbd2c7ffc02c -r 4a8743618257 src/HOL/Matrix/Matrix.thy
--- a/src/HOL/Matrix/Matrix.thy	Wed Nov 30 16:05:15 2011 +0100
+++ b/src/HOL/Matrix/Matrix.thy	Wed Nov 30 16:27:10 2011 +0100
@@ -11,18 +11,19 @@
 definition nonzero_positions :: "(nat \<Rightarrow> nat \<Rightarrow> 'a::zero) \<Rightarrow> (nat \<times> nat) set" where
   "nonzero_positions A = {pos. A (fst pos) (snd pos) ~= 0}"
 
-typedef 'a matrix = "{(f::(nat \<Rightarrow> nat \<Rightarrow> 'a::zero)). finite (nonzero_positions f)}"
-proof -
-  have "(\<lambda>j i. 0) \<in> {(f::(nat \<Rightarrow> nat \<Rightarrow> 'a::zero)). finite (nonzero_positions f)}"
+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"
+  unfolding matrix_def
+proof
+  show "(\<lambda>j i. 0) \<in> {(f::(nat \<Rightarrow> nat \<Rightarrow> 'a::zero)). finite (nonzero_positions f)}"
     by (simp add: nonzero_positions_def)
-  then show ?thesis by auto
 qed
 
 declare Rep_matrix_inverse[simp]
 
 lemma finite_nonzero_positions : "finite (nonzero_positions (Rep_matrix A))"
-apply (rule Abs_matrix_induct)
-by (simp add: Abs_matrix_inverse matrix_def)
+  by (induct A) (simp add: Abs_matrix_inverse matrix_def)
 
 definition nrows :: "('a::zero) matrix \<Rightarrow> nat" where
   "nrows A == if nonzero_positions(Rep_matrix A) = {} then 0 else Suc(Max ((image fst) (nonzero_positions (Rep_matrix A))))"
diff -r bbd2c7ffc02c -r 4a8743618257 src/HOL/Multivariate_Analysis/Finite_Cartesian_Product.thy
--- a/src/HOL/Multivariate_Analysis/Finite_Cartesian_Product.thy	Wed Nov 30 16:05:15 2011 +0100
+++ b/src/HOL/Multivariate_Analysis/Finite_Cartesian_Product.thy	Wed Nov 30 16:27:10 2011 +0100
@@ -13,8 +13,7 @@
 
 subsection {* Finite Cartesian products, with indexing and lambdas. *}
 
-typedef (open)
-  ('a, 'b) vec = "UNIV :: (('b::finite) \<Rightarrow> 'a) set"
+typedef (open) ('a, 'b) vec = "UNIV :: (('b::finite) \<Rightarrow> 'a) set"
   morphisms vec_nth vec_lambda ..
 
 notation
diff -r bbd2c7ffc02c -r 4a8743618257 src/HOL/NSA/StarDef.thy
--- a/src/HOL/NSA/StarDef.thy	Wed Nov 30 16:05:15 2011 +0100
+++ b/src/HOL/NSA/StarDef.thy	Wed Nov 30 16:27:10 2011 +0100
@@ -39,8 +39,10 @@
   starrel :: "((nat \<Rightarrow> 'a) \<times> (nat \<Rightarrow> 'a)) set" where
   "starrel = {(X,Y). {n. X n = Y n} \<in> \<U>}"
 
-typedef 'a star = "(UNIV :: (nat \<Rightarrow> 'a) set) // starrel"
-by (auto intro: quotientI)
+definition "star = (UNIV :: (nat \<Rightarrow> 'a) set) // starrel"
+
+typedef (open) 'a star = "star :: (nat \<Rightarrow> 'a) set set"
+  unfolding star_def by (auto intro: quotientI)
 
 definition
   star_n :: "(nat \<Rightarrow> 'a) \<Rightarrow> 'a star" where
diff -r bbd2c7ffc02c -r 4a8743618257 src/HOL/Nitpick_Examples/Manual_Nits.thy
--- a/src/HOL/Nitpick_Examples/Manual_Nits.thy	Wed Nov 30 16:05:15 2011 +0100
+++ b/src/HOL/Nitpick_Examples/Manual_Nits.thy	Wed Nov 30 16:27:10 2011 +0100
@@ -95,8 +95,9 @@
 
 subsection {* 2.7. Typedefs, Records, Rationals, and Reals *}
 
-typedef three = "{0\<Colon>nat, 1, 2}"
-by blast
+definition "three = {0\<Colon>nat, 1, 2}"
+typedef (open) three = three
+unfolding three_def by blast
 
 definition A :: three where "A \<equiv> Abs_three 0"
 definition B :: three where "B \<equiv> Abs_three 1"
@@ -197,7 +198,10 @@
    axiomatization. The examples also work unchanged with Lochbihler's
    "Coinductive_List" theory. *)
 
-typedef 'a llist = "UNIV\<Colon>('a list + (nat \<Rightarrow> 'a)) set" by auto
+definition "llist = (UNIV\<Colon>('a list + (nat \<Rightarrow> 'a)) set)"
+
+typedef (open) 'a llist = "llist\<Colon>('a list + (nat \<Rightarrow> 'a)) set"
+unfolding llist_def by auto
 
 definition LNil where
 "LNil = Abs_llist (Inl [])"
diff -r bbd2c7ffc02c -r 4a8743618257 src/HOL/Nitpick_Examples/Refute_Nits.thy
--- a/src/HOL/Nitpick_Examples/Refute_Nits.thy	Wed Nov 30 16:05:15 2011 +0100
+++ b/src/HOL/Nitpick_Examples/Refute_Nits.thy	Wed Nov 30 16:27:10 2011 +0100
@@ -539,8 +539,10 @@
 
 text {* A completely unspecified non-empty subset of @{typ "'a"}: *}
 
-typedef 'a myTdef = "insert (undefined\<Colon>'a) (undefined\<Colon>'a set)"
-by auto
+definition "myTdef = insert (undefined::'a) (undefined::'a set)"
+
+typedef (open) 'a myTdef = "myTdef :: 'a set"
+unfolding myTdef_def by auto
 
 lemma "(x\<Colon>'a myTdef) = y"
 nitpick [expect = genuine]
@@ -548,8 +550,10 @@
 
 typedecl myTdecl
 
-typedef 'a T_bij = "{(f\<Colon>'a\<Rightarrow>'a). \<forall>y. \<exists>!x. f x = y}"
-by auto
+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"
+unfolding T_bij_def by auto
 
 lemma "P (f\<Colon>(myTdecl myTdef) T_bij)"
 nitpick [expect = genuine]
diff -r bbd2c7ffc02c -r 4a8743618257 src/HOL/Nitpick_Examples/Typedef_Nits.thy
--- a/src/HOL/Nitpick_Examples/Typedef_Nits.thy	Wed Nov 30 16:05:15 2011 +0100
+++ b/src/HOL/Nitpick_Examples/Typedef_Nits.thy	Wed Nov 30 16:27:10 2011 +0100
@@ -14,8 +14,9 @@
 nitpick_params [verbose, card = 1\<emdash>4, sat_solver = MiniSat_JNI, max_threads = 1,
                 timeout = 240]
 
-typedef three = "{0\<Colon>nat, 1, 2}"
-by blast
+definition "three = {0\<Colon>nat, 1, 2}"
+typedef (open) three = three
+unfolding three_def by blast
 
 definition A :: three where "A \<equiv> Abs_three 0"
 definition B :: three where "B \<equiv> Abs_three 1"
@@ -25,8 +26,10 @@
 nitpick [expect = genuine]
 oops
 
-typedef 'a one_or_two = "{undefined False\<Colon>'a, undefined True}"
-by auto
+definition "one_or_two = {undefined False\<Colon>'a, undefined True}"
+
+typedef (open) 'a one_or_two = "one_or_two :: 'a set"
+unfolding one_or_two_def by auto
 
 lemma "x = (y\<Colon>unit one_or_two)"
 nitpick [expect = none]
@@ -49,8 +52,9 @@
 nitpick [card = 2, expect = none]
 oops
 
-typedef 'a bounded =
-        "{n\<Colon>nat. finite (UNIV\<Colon>'a \<Rightarrow> bool) \<longrightarrow> n < card (UNIV\<Colon>'a \<Rightarrow> bool)}"
+definition "bounded = {n\<Colon>nat. finite (UNIV\<Colon>'a \<Rightarrow> bool) \<longrightarrow> n < card (UNIV\<Colon>'a \<Rightarrow> bool)}"
+typedef (open) 'a bounded = "bounded(TYPE('a))"
+unfolding bounded_def
 apply (rule_tac x = 0 in exI)
 apply (case_tac "card UNIV = 0")
 by auto
diff -r bbd2c7ffc02c -r 4a8743618257 src/HOL/Nominal/Nominal.thy
--- a/src/HOL/Nominal/Nominal.thy	Wed Nov 30 16:05:15 2011 +0100
+++ b/src/HOL/Nominal/Nominal.thy	Wed Nov 30 16:27:10 2011 +0100
@@ -3395,8 +3395,12 @@
   where
   ABS_in: "(abs_fun a x)\<in>ABS_set"
 
-typedef (ABS) ('x,'a) ABS ("\<guillemotleft>_\<guillemotright>_" [1000,1000] 1000) =
-  "ABS_set::('x\<Rightarrow>('a noption)) set"
+definition "ABS = ABS_set"
+
+typedef (open) ('x,'a) ABS ("\<guillemotleft>_\<guillemotright>_" [1000,1000] 1000) =
+    "ABS::('x\<Rightarrow>('a noption)) set"
+  morphisms Rep_ABS Abs_ABS
+  unfolding ABS_def
 proof 
   fix x::"'a" and a::"'x"
   show "(abs_fun a x)\<in> ABS_set" by (rule ABS_in)
diff -r bbd2c7ffc02c -r 4a8743618257 src/HOL/Product_Type.thy
--- a/src/HOL/Product_Type.thy	Wed Nov 30 16:05:15 2011 +0100
+++ b/src/HOL/Product_Type.thy	Wed Nov 30 16:27:10 2011 +0100
@@ -46,14 +46,10 @@
 subsection {* The @{text unit} type *}
 
 typedef (open) unit = "{True}"
-proof
-  show "True : ?unit" ..
-qed
+  by auto
 
-definition
-  Unity :: unit    ("'(')")
-where
-  "() = Abs_unit True"
+definition Unity :: unit  ("'(')")
+  where "() = Abs_unit True"
 
 lemma unit_eq [no_atp]: "u = ()"
   by (induct u) (simp add: Unity_def)
@@ -136,12 +132,8 @@
 definition Pair_Rep :: "'a \<Rightarrow> 'b \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> bool" where
   "Pair_Rep a b = (\<lambda>x y. x = a \<and> y = b)"
 
-typedef ('a, 'b) prod (infixr "*" 20)
-  = "{f. \<exists>a b. f = Pair_Rep (a\<Colon>'a) (b\<Colon>'b)}"
-proof
-  fix a b show "Pair_Rep a b \<in> ?prod"
-    by rule+
-qed
+typedef ('a, 'b) prod (infixr "*" 20) = "{f. \<exists>a b. f = Pair_Rep (a\<Colon>'a) (b\<Colon>'b)}"
+  by auto
 
 type_notation (xsymbols)
   "prod"  ("(_ \<times>/ _)" [21, 20] 20)
diff -r bbd2c7ffc02c -r 4a8743618257 src/HOL/Quotient_Examples/Lift_Set.thy
--- a/src/HOL/Quotient_Examples/Lift_Set.thy	Wed Nov 30 16:05:15 2011 +0100
+++ b/src/HOL/Quotient_Examples/Lift_Set.thy	Wed Nov 30 16:27:10 2011 +0100
@@ -8,21 +8,29 @@
 imports Main
 begin
 
-typedef 'a set = "(UNIV :: ('a => bool) => bool)"
-morphisms member Set by auto
+definition set where "set = (UNIV :: ('a => bool) => bool)"
+
+typedef (open) 'a set = "set :: 'a set set"
+  morphisms member Set
+  unfolding set_def by auto
 
 text {* Here is some ML setup that should eventually be incorporated in the typedef command. *}
 
 local_setup {* fn lthy =>
-let
-  val quotients = {qtyp = @{typ "'a set"}, rtyp = @{typ "'a => bool"}, equiv_rel = @{term "dummy"}, equiv_thm = @{thm refl}}
-  val qty_full_name = @{type_name "set"}
+  let
+    val quotients =
+      {qtyp = @{typ "'a set"}, rtyp = @{typ "'a => bool"},
+        equiv_rel = @{term "dummy"}, equiv_thm = @{thm refl}}
+    val qty_full_name = @{type_name "set"}
 
-  fun qinfo phi = Quotient_Info.transform_quotients phi quotients
-  in lthy
+    fun qinfo phi = Quotient_Info.transform_quotients phi quotients
+  in
+    lthy
     |> Local_Theory.declaration {syntax = false, pervasive = true}
-        (fn phi => Quotient_Info.update_quotients qty_full_name (qinfo phi)
-       #> Quotient_Info.update_abs_rep qty_full_name (Quotient_Info.transform_abs_rep phi {abs = @{term "Set"}, rep = @{term "member"}}))
+        (fn phi =>
+          Quotient_Info.update_quotients qty_full_name (qinfo phi) #>
+          Quotient_Info.update_abs_rep qty_full_name
+            (Quotient_Info.transform_abs_rep phi {abs = @{term "Set"}, rep = @{term "member"}}))
   end
 *}
 
diff -r bbd2c7ffc02c -r 4a8743618257 src/HOL/Rat.thy
--- a/src/HOL/Rat.thy	Wed Nov 30 16:05:15 2011 +0100
+++ b/src/HOL/Rat.thy	Wed Nov 30 16:27:10 2011 +0100
@@ -54,7 +54,11 @@
   shows "ratrel `` {x} = ratrel `` {y} \<longleftrightarrow> (x, y) \<in> ratrel"
   by (rule eq_equiv_class_iff, rule equiv_ratrel) (auto simp add: assms)
 
-typedef (Rat) rat = "{x. snd x \<noteq> 0} // ratrel"
+definition "Rat = {x. snd x \<noteq> 0} // ratrel"
+
+typedef (open) rat = Rat
+  morphisms Rep_Rat Abs_Rat
+  unfolding Rat_def
 proof
   have "(0::int, 1::int) \<in> {x. snd x \<noteq> 0}" by simp
   then show "ratrel `` {(0, 1)} \<in> {x. snd x \<noteq> 0} // ratrel" by (rule quotientI)
diff -r bbd2c7ffc02c -r 4a8743618257 src/HOL/SMT_Examples/SMT_Tests.thy
--- a/src/HOL/SMT_Examples/SMT_Tests.thy	Wed Nov 30 16:05:15 2011 +0100
+++ b/src/HOL/SMT_Examples/SMT_Tests.thy	Wed Nov 30 16:27:10 2011 +0100
@@ -762,7 +762,10 @@
 
 subsubsection {* Type definitions *}
 
-typedef three = "{1, 2, 3::int}" by auto
+definition "three = {1, 2, 3::int}"
+
+typedef (open) three = three
+  unfolding three_def by auto
 
 definition n1 where "n1 = Abs_three 1"
 definition n2 where "n2 = Abs_three 2"
diff -r bbd2c7ffc02c -r 4a8743618257 src/HOL/Sum_Type.thy
--- a/src/HOL/Sum_Type.thy	Wed Nov 30 16:05:15 2011 +0100
+++ b/src/HOL/Sum_Type.thy	Wed Nov 30 16:27:10 2011 +0100
@@ -17,8 +17,10 @@
 definition Inr_Rep :: "'b \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> bool \<Rightarrow> bool" where
   "Inr_Rep b x y p \<longleftrightarrow> y = b \<and> \<not> p"
 
-typedef ('a, 'b) sum (infixr "+" 10) = "{f. (\<exists>a. f = Inl_Rep (a::'a)) \<or> (\<exists>b. f = Inr_Rep (b::'b))}"
-  by auto
+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"
+  unfolding sum_def by auto
 
 lemma Inl_RepI: "Inl_Rep a \<in> sum"
   by (auto simp add: sum_def)
diff -r bbd2c7ffc02c -r 4a8743618257 src/HOL/UNITY/UNITY.thy
--- a/src/HOL/UNITY/UNITY.thy	Wed Nov 30 16:05:15 2011 +0100
+++ b/src/HOL/UNITY/UNITY.thy	Wed Nov 30 16:27:10 2011 +0100
@@ -12,10 +12,14 @@
 
 theory UNITY imports Main begin
 
-typedef (Program)
-  'a program = "{(init:: 'a set, acts :: ('a * 'a)set set,
-                   allowed :: ('a * 'a)set set). Id \<in> acts & Id: allowed}" 
-  by blast
+definition
+  "Program =
+    {(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"
+  morphisms Rep_Program Abs_Program
+  unfolding Program_def by blast
 
 definition Acts :: "'a program => ('a * 'a)set set" where
     "Acts F == (%(init, acts, allowed). acts) (Rep_Program F)"
diff -r bbd2c7ffc02c -r 4a8743618257 src/HOL/Word/Word.thy
--- a/src/HOL/Word/Word.thy	Wed Nov 30 16:05:15 2011 +0100
+++ b/src/HOL/Word/Word.thy	Wed Nov 30 16:27:10 2011 +0100
@@ -17,7 +17,7 @@
 
 subsection {* Type definition *}
 
-typedef (open word) 'a word = "{(0::int) ..< 2^len_of TYPE('a::len0)}"
+typedef (open) 'a word = "{(0::int) ..< 2^len_of TYPE('a::len0)}"
   morphisms uint Abs_word by auto
 
 definition word_of_int :: "int \<Rightarrow> 'a\<Colon>len0 word" where
diff -r bbd2c7ffc02c -r 4a8743618257 src/HOL/ZF/Games.thy
--- a/src/HOL/ZF/Games.thy	Wed Nov 30 16:05:15 2011 +0100
+++ b/src/HOL/ZF/Games.thy	Wed Nov 30 16:27:10 2011 +0100
@@ -189,8 +189,10 @@
   apply (simp add: games_lfp_unfold[symmetric])
   done
 
-typedef game = games_lfp
-  by (blast intro: games_lfp_nonempty)
+definition "game = games_lfp"
+
+typedef (open) game = game
+  unfolding game_def by (blast intro: games_lfp_nonempty)
 
 definition left_options :: "game \<Rightarrow> game zet" where
   "left_options g \<equiv> zimage Abs_game (zexplode (Fst (Rep_game g)))"
@@ -839,8 +841,10 @@
 definition eq_game_rel :: "(game * game) set" where
   "eq_game_rel \<equiv> { (p, q) . eq_game p q }"
 
-typedef Pg = "UNIV//eq_game_rel"
-  by (auto simp add: quotient_def)
+definition "Pg = UNIV//eq_game_rel"
+
+typedef (open) Pg = Pg
+  unfolding Pg_def by (auto simp add: quotient_def)
 
 lemma equiv_eq_game[simp]: "equiv UNIV eq_game_rel"
   by (auto simp add: equiv_def refl_on_def sym_def trans_def eq_game_rel_def
diff -r bbd2c7ffc02c -r 4a8743618257 src/HOL/ZF/Zet.thy
--- a/src/HOL/ZF/Zet.thy	Wed Nov 30 16:05:15 2011 +0100
+++ b/src/HOL/ZF/Zet.thy	Wed Nov 30 16:27:10 2011 +0100
@@ -9,8 +9,10 @@
 imports HOLZF
 begin
 
-typedef 'a zet = "{A :: 'a set | A f z. inj_on f A \<and> f ` A \<subseteq> explode z}"
-  by blast
+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"
+  unfolding zet_def by blast
 
 definition zin :: "'a \<Rightarrow> 'a zet \<Rightarrow> bool" where
   "zin x A == x \<in> (Rep_zet A)"
diff -r bbd2c7ffc02c -r 4a8743618257 src/HOL/ex/Dedekind_Real.thy
--- a/src/HOL/ex/Dedekind_Real.thy	Wed Nov 30 16:05:15 2011 +0100
+++ b/src/HOL/ex/Dedekind_Real.thy	Wed Nov 30 16:27:10 2011 +0100
@@ -44,8 +44,10 @@
 qed
 
 
-typedef preal = "{A. cut A}"
-  by (blast intro: cut_of_rat [OF zero_less_one])
+definition "preal = {A. cut A}"
+
+typedef (open) preal = preal
+  unfolding preal_def by (blast intro: cut_of_rat [OF zero_less_one])
 
 definition
   psup :: "preal set => preal" where
@@ -113,22 +115,26 @@
 by (simp add: preal_def cut_of_rat)
 
 lemma preal_nonempty: "A \<in> preal ==> \<exists>x\<in>A. 0 < x"
-by (unfold preal_def cut_def, blast)
+  unfolding preal_def cut_def_raw by blast
 
 lemma preal_Ex_mem: "A \<in> preal \<Longrightarrow> \<exists>x. x \<in> A"
-by (drule preal_nonempty, fast)
+  apply (drule preal_nonempty)
+  apply fast
+  done
 
 lemma preal_imp_psubset_positives: "A \<in> preal ==> A < {r. 0 < r}"
-by (force simp add: preal_def cut_def)
+  by (force simp add: preal_def cut_def)
 
 lemma preal_exists_bound: "A \<in> preal ==> \<exists>x. 0 < x & x \<notin> A"
-by (drule preal_imp_psubset_positives, auto)
+  apply (drule preal_imp_psubset_positives)
+  apply auto
+  done
 
 lemma preal_exists_greater: "[| A \<in> preal; y \<in> A |] ==> \<exists>u \<in> A. y < u"
-by (unfold preal_def cut_def, blast)
+  unfolding preal_def cut_def_raw by blast
 
 lemma preal_downwards_closed: "[| A \<in> preal; y \<in> A; 0 < z; z < y |] ==> z \<in> A"
-by (unfold preal_def cut_def, blast)
+  unfolding preal_def cut_def_raw by blast
 
 text{*Relaxing the final premise*}
 lemma preal_downwards_closed':
@@ -960,7 +966,7 @@
 
 lemma mem_diff_set:
      "R < S ==> diff_set (Rep_preal S) (Rep_preal R) \<in> preal"
-apply (unfold preal_def cut_def)
+apply (unfold preal_def cut_def_raw)
 apply (blast intro!: diff_set_not_empty diff_set_not_rat_set
                      diff_set_lemma3 diff_set_lemma4)
 done
@@ -1129,7 +1135,7 @@
 
 lemma preal_sup:
      "[|P \<noteq> {}; \<forall>X \<in> P. X \<le> Y|] ==> (\<Union>X \<in> P. Rep_preal(X)) \<in> preal"
-apply (unfold preal_def cut_def)
+apply (unfold preal_def cut_def_raw)
 apply (blast intro!: preal_sup_set_not_empty preal_sup_set_not_rat_set
                      preal_sup_set_lemma3 preal_sup_set_lemma4)
 done
@@ -1163,8 +1169,11 @@
   realrel   ::  "((preal * preal) * (preal * preal)) set" where
   "realrel = {p. \<exists>x1 y1 x2 y2. p = ((x1,y1),(x2,y2)) & x1+y2 = x2+y1}"
 
-typedef (Real)  real = "UNIV//realrel"
-  by (auto simp add: quotient_def)
+definition "Real = UNIV//realrel"
+
+typedef (open) real = Real
+  morphisms Rep_Real Abs_Real
+  unfolding Real_def by (auto simp add: quotient_def)
 
 definition
   (** these don't use the overloaded "real" function: users don't see them **)
diff -r bbd2c7ffc02c -r 4a8743618257 src/HOL/ex/PER.thy
--- a/src/HOL/ex/PER.thy	Wed Nov 30 16:05:15 2011 +0100
+++ b/src/HOL/ex/PER.thy	Wed Nov 30 16:27:10 2011 +0100
@@ -151,8 +151,10 @@
   \emph{equivalence classes} over elements of the base type @{typ 'a}.
 *}
 
-typedef 'a quot = "{{x. a \<sim> x}| a::'a::partial_equiv. True}"
-  by blast
+definition "quot = {{x. a \<sim> x}| a::'a::partial_equiv. True}"
+
+typedef (open) 'a quot = "quot :: 'a::partial_equiv set set"
+  unfolding quot_def by blast
 
 lemma quotI [intro]: "{x. a \<sim> x} \<in> quot"
   unfolding quot_def by blast
diff -r bbd2c7ffc02c -r 4a8743618257 src/HOL/ex/Refute_Examples.thy
--- a/src/HOL/ex/Refute_Examples.thy	Wed Nov 30 16:05:15 2011 +0100
+++ b/src/HOL/ex/Refute_Examples.thy	Wed Nov 30 16:27:10 2011 +0100
@@ -494,8 +494,10 @@
 
 text {* A completely unspecified non-empty subset of @{typ "'a"}: *}
 
-typedef 'a myTdef = "insert (undefined::'a) (undefined::'a set)"
-  by auto
+definition "myTdef = insert (undefined::'a) (undefined::'a set)"
+
+typedef (open) 'a myTdef = "myTdef :: 'a set"
+  unfolding myTdef_def by auto
 
 lemma "(x::'a myTdef) = y"
   refute
@@ -503,8 +505,10 @@
 
 typedecl myTdecl
 
-typedef 'a T_bij = "{(f::'a\<Rightarrow>'a). \<forall>y. \<exists>!x. f x = y}"
-  by auto
+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"
+  unfolding T_bij_def by auto
 
 lemma "P (f::(myTdecl myTdef) T_bij)"
   refute