changeset 8920 | af5e09b6c208 |
parent 8919 | d00b01ed8539 |
child 8921 | 7c04c98132c4 |
--- a/src/HOL/AxClasses/Tutorial/Xor.thy Mon May 22 13:20:47 2000 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,15 +0,0 @@ -(* Title: HOL/AxClasses/Tutorial/Xor.thy - ID: $Id$ - Author: Markus Wenzel, TU Muenchen - -Define overloaded constants "<*>", "inverse", "1" on type "bool". -*) - -Xor = Group + - -defs - prod_bool_def "x <*> y == x ~= (y::bool)" - inverse_bool_def "inverse x == x::bool" - unit_bool_def "1 == False" - -end