renamed "()" to Unity, made local;
authorwenzelm
Thu Sep 27 22:22:58 2001 +0200 (2001-09-27)
changeset 11602bf6700f4c010
parent 11601 9273cef990f5
child 11603 c3724decadef
renamed "()" to Unity, made local;
src/HOL/Product_Type.thy
     1.1 --- a/src/HOL/Product_Type.thy	Thu Sep 27 22:22:08 2001 +0200
     1.2 +++ b/src/HOL/Product_Type.thy	Thu Sep 27 22:22:58 2001 +0200
     1.3 @@ -96,21 +96,15 @@
     1.4  
     1.5  (** unit **)
     1.6  
     1.7 -global
     1.8 -
     1.9  typedef unit = "{True}"
    1.10  proof
    1.11    show "True : ?unit"
    1.12      by blast
    1.13  qed
    1.14  
    1.15 -consts
    1.16 -  "()"          :: unit                           ("'(')")
    1.17 -
    1.18 -local
    1.19 -
    1.20 -defs
    1.21 -  Unity_def:    "() == Abs_unit True"
    1.22 +constdefs
    1.23 +  Unity :: unit    ("'(')")
    1.24 +  "() == Abs_unit True"
    1.25  
    1.26  
    1.27