changeset 1247 | 18b1441fb603 |
child 2907 | 0e272e4c7cb2 |
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 |