src/HOL/Prod.thy
changeset 3947 eb707467f8c5
parent 3842 b55686a7b22c
child 4570 c04027ccc86e
     1.1 --- a/src/HOL/Prod.thy	Mon Oct 20 11:22:29 1997 +0200
     1.2 +++ b/src/HOL/Prod.thy	Mon Oct 20 11:25:39 1997 +0200
     1.3 @@ -18,6 +18,8 @@
     1.4    Pair_Rep      :: ['a, 'b] => ['a, 'b] => bool
     1.5    "Pair_Rep == (%a b. %x y. x=a & y=b)"
     1.6  
     1.7 +global
     1.8 +
     1.9  typedef (Prod)
    1.10    ('a, 'b) "*"          (infixr 20)
    1.11      = "{f. ? a b. f = Pair_Rep (a::'a) (b::'b)}"
    1.12 @@ -71,6 +73,8 @@
    1.13  
    1.14  (* definitions *)
    1.15  
    1.16 +local
    1.17 +
    1.18  defs
    1.19    Pair_def      "Pair a b == Abs_Prod(Pair_Rep a b)"
    1.20    fst_def       "fst p == @a. ? b. p = (a, b)"
    1.21 @@ -83,11 +87,15 @@
    1.22  
    1.23  (** unit **)
    1.24  
    1.25 +global
    1.26 +
    1.27  typedef  unit = "{True}"
    1.28  
    1.29  consts
    1.30    "()"          :: unit                           ("'(')")
    1.31  
    1.32 +local
    1.33 +
    1.34  defs
    1.35    Unity_def     "() == Abs_unit True"
    1.36