Now: unit = {True}
authornipkow
Thu Apr 03 19:29:53 1997 +0200 (1997-04-03)
changeset 2886fd5645efa43d
parent 2885 8d229dc0cfe2
child 2887 00b8ee790d89
Now: unit = {True}
src/HOL/Prod.ML
src/HOL/Prod.thy
     1.1 --- a/src/HOL/Prod.ML	Thu Apr 03 10:36:54 1997 +0200
     1.2 +++ b/src/HOL/Prod.ML	Thu Apr 03 19:29:53 1997 +0200
     1.3 @@ -302,7 +302,7 @@
     1.4  
     1.5  goalw Prod.thy [Unity_def]
     1.6      "u = ()";
     1.7 -by (stac (rewrite_rule [unit_def] Rep_unit RS CollectD RS sym) 1);
     1.8 +by (stac (rewrite_rule [unit_def] Rep_unit RS singletonD RS sym) 1);
     1.9  by (rtac (Rep_unit_inverse RS sym) 1);
    1.10  qed "unit_eq";
    1.11   
     2.1 --- a/src/HOL/Prod.thy	Thu Apr 03 10:36:54 1997 +0200
     2.2 +++ b/src/HOL/Prod.thy	Thu Apr 03 19:29:53 1997 +0200
     2.3 @@ -79,7 +79,7 @@
     2.4  
     2.5  (** unit **)
     2.6  
     2.7 -typedef  unit = "{p. p = True}"
     2.8 +typedef  unit = "{True}"
     2.9  
    2.10  consts
    2.11    "()"          :: unit                           ("'(')")