Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Now: unit = {True}
authornipkow
Thu, 03 Apr 1997 19:29:53 +0200
changeset 2886 fd5645efa43d
parent 2885 8d229dc0cfe2
child 2887 00b8ee790d89
Now: unit = {True}
src/HOL/Prod.ML file | annotate | diff | comparison | revisions
src/HOL/Prod.thy file | annotate | diff | comparison | revisions 
--- a/src/HOL/Prod.ML	Thu Apr 03 10:36:54 1997 +0200
+++ b/src/HOL/Prod.ML	Thu Apr 03 19:29:53 1997 +0200
@@ -302,7 +302,7 @@
 
 goalw Prod.thy [Unity_def]
     "u = ()";
-by (stac (rewrite_rule [unit_def] Rep_unit RS CollectD RS sym) 1);
+by (stac (rewrite_rule [unit_def] Rep_unit RS singletonD RS sym) 1);
 by (rtac (Rep_unit_inverse RS sym) 1);
 qed "unit_eq";
  
--- a/src/HOL/Prod.thy	Thu Apr 03 10:36:54 1997 +0200
+++ b/src/HOL/Prod.thy	Thu Apr 03 19:29:53 1997 +0200
@@ -79,7 +79,7 @@
 
 (** unit **)
 
-typedef  unit = "{p. p = True}"
+typedef  unit = "{True}"
 
 consts
   "()"          :: unit                           ("'(')")
isabelle