src/HOL/AxClasses/Tutorial/Xor.thy
changeset 1247 18b1441fb603
child 2907 0e272e4c7cb2
equal deleted inserted replaced
1246:706cfddca75c 1247:18b1441fb603
       
     1 (*  Title:      HOL/AxClasses/Tutorial/Xor.thy
       
     2     ID:         $Id$
       
     3     Author:     Markus Wenzel, TU Muenchen
       
     4 
       
     5 Define overloaded constants "<*>", "inv", "1" on type "bool".
       
     6 *)
       
     7 
       
     8 Xor = Group +
       
     9 
       
    10 defs
       
    11   prod_bool_def "x <*> y == x ~= (y::bool)"
       
    12   inv_bool_def  "inv x   == x::bool"
       
    13   unit_bool_def "1       == False"
       
    14 
       
    15 end