# HG changeset patch
# User berghofe
# Date 909174858 -7200
# Node ID bf5d9e5b8cdf2b619738899be9daa4cacee7e27c
# Parent  27a2b36efd95011709cf31627e75590d6143799d
unit and bool are now represented as datatypes.

diff -r 27a2b36efd95 -r bf5d9e5b8cdf src/HOL/Datatype.thy
--- 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