src/ZF/Bool.thy
changeset 13328 703de709a64b
parent 13269 3ba9be497c33
child 13356 c9cfe1638bf2
equal deleted inserted replaced
13327:be7105a066d3 13328:703de709a64b
     1 (*  Title:      ZF/bool.thy
     1 (*  Title:      ZF/bool.thy
     2     ID:         $Id$
     2     ID:         $Id$
     3     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     3     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     4     Copyright   1992  University of Cambridge
     4     Copyright   1992  University of Cambridge
     5 
     5 
     6 Booleans in Zermelo-Fraenkel Set Theory 
       
     7 
       
     8 2 is equal to bool, but serves a different purpose
       
     9 *)
     6 *)
       
     7 
       
     8 header{*Booleans in Zermelo-Fraenkel Set Theory*}
    10 
     9 
    11 theory Bool = pair:
    10 theory Bool = pair:
    12 
    11 
    13 syntax
    12 syntax
    14     "1"         :: i             ("1")
    13     "1"         :: i             ("1")
    15     "2"         :: i             ("2")
    14     "2"         :: i             ("2")
    16 
    15 
    17 translations
    16 translations
    18    "1"  == "succ(0)"
    17    "1"  == "succ(0)"
    19    "2"  == "succ(1)"
    18    "2"  == "succ(1)"
       
    19 
       
    20 text{*2 is equal to bool, but is used as a number rather than a type.*}
    20 
    21 
    21 constdefs
    22 constdefs
    22   bool        :: i
    23   bool        :: i
    23     "bool == {0,1}"
    24     "bool == {0,1}"
    24 
    25