--- a/src/HOL/Nat.thy Wed Nov 30 17:30:01 2011 +0100
+++ b/src/HOL/Nat.thy Wed Nov 30 18:07:14 2011 +0100
@@ -35,7 +35,8 @@
Zero_RepI: "Nat Zero_Rep"
| Suc_RepI: "Nat i \<Longrightarrow> Nat (Suc_Rep i)"
-typedef (open Nat) nat = "{n. Nat n}"
+typedef (open) nat = "{n. Nat n}"
+ morphisms Rep_Nat Abs_Nat
using Nat.Zero_RepI by auto
lemma Nat_Rep_Nat:
--- a/src/HOL/Product_Type.thy Wed Nov 30 17:30:01 2011 +0100
+++ b/src/HOL/Product_Type.thy Wed Nov 30 18:07:14 2011 +0100
@@ -132,8 +132,10 @@
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)}"
- by auto
+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"
+ unfolding prod_def by auto
type_notation (xsymbols)
"prod" ("(_ \<times>/ _)" [21, 20] 20)