prefer typedef without alternative name;
authorwenzelm
Wed Nov 30 18:07:14 2011 +0100 (2011-11-30)
changeset 45696476ad865f125
parent 45695 b108b3d7c49e
child 45699 3e006216319f
prefer typedef without alternative name;
src/HOL/Nat.thy
src/HOL/Product_Type.thy
     1.1 --- a/src/HOL/Nat.thy	Wed Nov 30 17:30:01 2011 +0100
     1.2 +++ b/src/HOL/Nat.thy	Wed Nov 30 18:07:14 2011 +0100
     1.3 @@ -35,7 +35,8 @@
     1.4    Zero_RepI: "Nat Zero_Rep"
     1.5  | Suc_RepI: "Nat i \<Longrightarrow> Nat (Suc_Rep i)"
     1.6  
     1.7 -typedef (open Nat) nat = "{n. Nat n}"
     1.8 +typedef (open) nat = "{n. Nat n}"
     1.9 +  morphisms Rep_Nat Abs_Nat
    1.10    using Nat.Zero_RepI by auto
    1.11  
    1.12  lemma Nat_Rep_Nat:
     2.1 --- a/src/HOL/Product_Type.thy	Wed Nov 30 17:30:01 2011 +0100
     2.2 +++ b/src/HOL/Product_Type.thy	Wed Nov 30 18:07:14 2011 +0100
     2.3 @@ -132,8 +132,10 @@
     2.4  definition Pair_Rep :: "'a \<Rightarrow> 'b \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> bool" where
     2.5    "Pair_Rep a b = (\<lambda>x y. x = a \<and> y = b)"
     2.6  
     2.7 -typedef ('a, 'b) prod (infixr "*" 20) = "{f. \<exists>a b. f = Pair_Rep (a\<Colon>'a) (b\<Colon>'b)}"
     2.8 -  by auto
     2.9 +definition "prod = {f. \<exists>a b. f = Pair_Rep (a\<Colon>'a) (b\<Colon>'b)}"
    2.10 +
    2.11 +typedef (open) ('a, 'b) prod (infixr "*" 20) = "prod :: ('a \<Rightarrow> 'b \<Rightarrow> bool) set"
    2.12 +  unfolding prod_def by auto
    2.13  
    2.14  type_notation (xsymbols)
    2.15    "prod"  ("(_ \<times>/ _)" [21, 20] 20)