src/HOL/Product_Type.thy
changeset 45696 476ad865f125
parent 45694 4a8743618257
child 45986 c9e50153e5ae
     1.1 --- a/src/HOL/Product_Type.thy	Wed Nov 30 17:30:01 2011 +0100
     1.2 +++ b/src/HOL/Product_Type.thy	Wed Nov 30 18:07:14 2011 +0100
     1.3 @@ -132,8 +132,10 @@
     1.4  definition Pair_Rep :: "'a \<Rightarrow> 'b \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> bool" where
     1.5    "Pair_Rep a b = (\<lambda>x y. x = a \<and> y = b)"
     1.6  
     1.7 -typedef ('a, 'b) prod (infixr "*" 20) = "{f. \<exists>a b. f = Pair_Rep (a\<Colon>'a) (b\<Colon>'b)}"
     1.8 -  by auto
     1.9 +definition "prod = {f. \<exists>a b. f = Pair_Rep (a\<Colon>'a) (b\<Colon>'b)}"
    1.10 +
    1.11 +typedef (open) ('a, 'b) prod (infixr "*" 20) = "prod :: ('a \<Rightarrow> 'b \<Rightarrow> bool) set"
    1.12 +  unfolding prod_def by auto
    1.13  
    1.14  type_notation (xsymbols)
    1.15    "prod"  ("(_ \<times>/ _)" [21, 20] 20)