author | wenzelm |
Fri, 01 Sep 1995 14:27:36 +0200 | |
changeset 1247 | 18b1441fb603 |
child 2907 | 0e272e4c7cb2 |
permissions | -rw-r--r-- |
1247 | 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 |