isabelle: src/HOL/AxClasses/Tutorial/Xor.ML@a901bafe4578 (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");
6393 b8dafa978382 fixed axclass_tac; wenzelm parents: 2907 diff changeset	11	by (axclass_tac []);
2907 0e272e4c7cb2 inv -> inverse nipkow parents: 1899 diff changeset	12	by (rewrite_goals_tac
0e272e4c7cb2 inv -> inverse nipkow parents: 1899 diff changeset	13	[Xor.prod_bool_def,Xor.inverse_bool_def, Xor.unit_bool_def]);
1899 0075a8d26a80 Classical tactics now use default claset. berghofe parents: 1247 diff changeset	14	by (ALLGOALS (Fast_tac));
1247 18b1441fb603 Various axiomatic type class demos; wenzelm parents: diff changeset	15	qed "bool_in_agroup";

author	wenzelm
	Mon, 29 Nov 1999 15:52:49 +0100
changeset 8039	a901bafe4578
parent 6393	b8dafa978382
permissions	-rw-r--r--