isabelle: src/HOL/AxClasses/Tutorial/Xor.thy@131f72e2cd56 (annotated)

1247 18b1441fb603 Various axiomatic type class demos; wenzelm parents: diff changeset	1	(* Title: HOL/AxClasses/Tutorial/Xor.thy
18b1441fb603 Various axiomatic type class demos; wenzelm parents: diff changeset	2	ID: $Id$
18b1441fb603 Various axiomatic type class demos; wenzelm parents: diff changeset	3	Author: Markus Wenzel, TU Muenchen
18b1441fb603 Various axiomatic type class demos; wenzelm parents: diff changeset	4
18b1441fb603 Various axiomatic type class demos; wenzelm parents: diff changeset	5	Define overloaded constants "<*>", "inv", "1" on type "bool".
18b1441fb603 Various axiomatic type class demos; wenzelm parents: diff changeset	6	*)
18b1441fb603 Various axiomatic type class demos; wenzelm parents: diff changeset	7
18b1441fb603 Various axiomatic type class demos; wenzelm parents: diff changeset	8	Xor = Group +
18b1441fb603 Various axiomatic type class demos; wenzelm parents: diff changeset	9
18b1441fb603 Various axiomatic type class demos; wenzelm parents: diff changeset	10	defs
18b1441fb603 Various axiomatic type class demos; wenzelm parents: diff changeset	11	prod_bool_def "x <*> y == x ~= (y::bool)"
18b1441fb603 Various axiomatic type class demos; wenzelm parents: diff changeset	12	inv_bool_def "inv x == x::bool"
18b1441fb603 Various axiomatic type class demos; wenzelm parents: diff changeset	13	unit_bool_def "1 == False"
18b1441fb603 Various axiomatic type class demos; wenzelm parents: diff changeset	14
18b1441fb603 Various axiomatic type class demos; wenzelm parents: diff changeset	15	end

author	clasohm
	Mon, 11 Sep 1995 12:38:20 +0200
changeset 1253	131f72e2cd56
parent 1247	18b1441fb603
child 2907	0e272e4c7cb2
permissions	-rw-r--r--