isabelle: src/HOL/AxClasses/Tutorial/Xor.ML@b5e43a60443a (annotated)

1247 18b1441fb603 Various axiomatic type class demos; wenzelm parents: diff changeset	1	(* Title: HOL/AxClasses/Tutorial/Xor.ML
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	Proof the instantiation theorem bool :: agroup by hand.
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	open AxClass;
18b1441fb603 Various axiomatic type class demos; wenzelm parents: diff changeset	9
18b1441fb603 Various axiomatic type class demos; wenzelm parents: diff changeset	10	goal_arity Xor.thy ("bool", [], "agroup");
18b1441fb603 Various axiomatic type class demos; wenzelm parents: diff changeset	11	by (axclass_tac Xor.thy []);
18b1441fb603 Various axiomatic type class demos; wenzelm parents: diff changeset	12	by (rewrite_goals_tac [Xor.prod_bool_def, Xor.inv_bool_def, Xor.unit_bool_def]);
18b1441fb603 Various axiomatic type class demos; wenzelm parents: diff changeset	13	by (ALLGOALS (fast_tac HOL_cs));
18b1441fb603 Various axiomatic type class demos; wenzelm parents: diff changeset	14	qed "bool_in_agroup";

author	paulson
	Fri, 29 Mar 1996 10:54:44 +0100
changeset 1629	b5e43a60443a
parent 1247	18b1441fb603
child 1899	0075a8d26a80
permissions	-rw-r--r--