src/HOL/Product_Type.thy
changeset 45694 4a8743618257
parent 45662 4f7c05990420
child 45696 476ad865f125
     1.1 --- a/src/HOL/Product_Type.thy	Wed Nov 30 16:05:15 2011 +0100
     1.2 +++ b/src/HOL/Product_Type.thy	Wed Nov 30 16:27:10 2011 +0100
     1.3 @@ -46,14 +46,10 @@
     1.4  subsection {* The @{text unit} type *}
     1.5  
     1.6  typedef (open) unit = "{True}"
     1.7 -proof
     1.8 -  show "True : ?unit" ..
     1.9 -qed
    1.10 +  by auto
    1.11  
    1.12 -definition
    1.13 -  Unity :: unit    ("'(')")
    1.14 -where
    1.15 -  "() = Abs_unit True"
    1.16 +definition Unity :: unit  ("'(')")
    1.17 +  where "() = Abs_unit True"
    1.18  
    1.19  lemma unit_eq [no_atp]: "u = ()"
    1.20    by (induct u) (simp add: Unity_def)
    1.21 @@ -136,12 +132,8 @@
    1.22  definition Pair_Rep :: "'a \<Rightarrow> 'b \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> bool" where
    1.23    "Pair_Rep a b = (\<lambda>x y. x = a \<and> y = b)"
    1.24  
    1.25 -typedef ('a, 'b) prod (infixr "*" 20)
    1.26 -  = "{f. \<exists>a b. f = Pair_Rep (a\<Colon>'a) (b\<Colon>'b)}"
    1.27 -proof
    1.28 -  fix a b show "Pair_Rep a b \<in> ?prod"
    1.29 -    by rule+
    1.30 -qed
    1.31 +typedef ('a, 'b) prod (infixr "*" 20) = "{f. \<exists>a b. f = Pair_Rep (a\<Colon>'a) (b\<Colon>'b)}"
    1.32 +  by auto
    1.33  
    1.34  type_notation (xsymbols)
    1.35    "prod"  ("(_ \<times>/ _)" [21, 20] 20)