src/HOL/AxClasses/Tutorial/Xor.thy
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