unit and bool are now represented as datatypes.
authorberghofe
Fri Oct 23 22:34:18 1998 +0200 (1998-10-23)
changeset 5759bf5d9e5b8cdf
parent 5758 27a2b36efd95
child 5760 7e2cf2820684
unit and bool are now represented as datatypes.
src/HOL/Datatype.thy
     1.1 --- a/src/HOL/Datatype.thy	Fri Oct 23 20:44:34 1998 +0200
     1.2 +++ b/src/HOL/Datatype.thy	Fri Oct 23 22:34:18 1998 +0200
     1.3 @@ -6,6 +6,10 @@
     1.4  
     1.5  Datatype = Univ +
     1.6  
     1.7 +rep_datatype bool
     1.8 +  distinct True_not_False, False_not_True
     1.9 +  induct   bool_induct
    1.10 +
    1.11  rep_datatype sum
    1.12    distinct Inl_not_Inr, Inr_not_Inl
    1.13    inject   Inl_eq, Inr_eq
    1.14 @@ -15,4 +19,7 @@
    1.15    inject   Pair_eq
    1.16    induct   prod_induct
    1.17  
    1.18 +rep_datatype unit
    1.19 +  induct   unit_induct
    1.20 +
    1.21  end