src/HOL/Prod.thy
changeset 2880 a0fde30aa126
parent 2393 651fce76c86c
child 2886 fd5645efa43d
     1.1 --- a/src/HOL/Prod.thy	Wed Apr 02 19:12:26 1997 +0200
     1.2 +++ b/src/HOL/Prod.thy	Thu Apr 03 09:46:42 1997 +0200
     1.3 @@ -79,14 +79,13 @@
     1.4  
     1.5  (** unit **)
     1.6  
     1.7 -typedef (Unit)
     1.8 -  unit = "{p. p = True}"
     1.9 +typedef  unit = "{p. p = True}"
    1.10  
    1.11  consts
    1.12    "()"          :: unit                           ("'(')")
    1.13  
    1.14  defs
    1.15 -  Unity_def     "() == Abs_Unit True"
    1.16 +  Unity_def     "() == Abs_unit True"
    1.17  
    1.18  end
    1.19