unit and bool are now represented as datatypes.

--- a/src/HOL/Datatype.thy	Fri Oct 23 20:44:34 1998 +0200
+++ b/src/HOL/Datatype.thy	Fri Oct 23 22:34:18 1998 +0200
@@ -6,6 +6,10 @@
 
 Datatype = Univ +
 
+rep_datatype bool
+  distinct True_not_False, False_not_True
+  induct   bool_induct
+
 rep_datatype sum
   distinct Inl_not_Inr, Inr_not_Inl
   inject   Inl_eq, Inr_eq
@@ -15,4 +19,7 @@
   inject   Pair_eq
   induct   prod_induct
 
+rep_datatype unit
+  induct   unit_induct
+
 end