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)
```