isabelle: src/HOL/AxClasses/Group/ROOT.ML@6cb15c6f1d9f (annotated)

1247 18b1441fb603 Various axiomatic type class demos; wenzelm parents: diff changeset	1	(* Title: HOL/AxClasses/Group/ROOT.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
1442 7a8a30b11a24 * empty log message * wenzelm parents: 1296 diff changeset	5	Some bits of group theory via axiomatic type classes.
1247 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	set show_types;
18b1441fb603 Various axiomatic type class demos; wenzelm parents: diff changeset	9	set show_sorts;
18b1441fb603 Various axiomatic type class demos; wenzelm parents: diff changeset	10
18b1441fb603 Various axiomatic type class demos; wenzelm parents: diff changeset	11	(disable bug compatibility)
18b1441fb603 Various axiomatic type class demos; wenzelm parents: diff changeset	12	reset force_strip_shyps;
18b1441fb603 Various axiomatic type class demos; wenzelm parents: diff changeset	13
1442 7a8a30b11a24 * empty log message * wenzelm parents: 1296 diff changeset	14	set force_strip_shyps; (* FIXME tmp hack *)
1247 18b1441fb603 Various axiomatic type class demos; wenzelm parents: diff changeset	15
18b1441fb603 Various axiomatic type class demos; wenzelm parents: diff changeset	16
18b1441fb603 Various axiomatic type class demos; wenzelm parents: diff changeset	17	use_thy "Sigs";
18b1441fb603 Various axiomatic type class demos; wenzelm parents: diff changeset	18
18b1441fb603 Various axiomatic type class demos; wenzelm parents: diff changeset	19	use_thy "Monoid";
18b1441fb603 Various axiomatic type class demos; wenzelm parents: diff changeset	20	use_thy "Group";
18b1441fb603 Various axiomatic type class demos; wenzelm parents: diff changeset	21
18b1441fb603 Various axiomatic type class demos; wenzelm parents: diff changeset	22	use_thy "MonoidGroupInsts";
18b1441fb603 Various axiomatic type class demos; wenzelm parents: diff changeset	23
18b1441fb603 Various axiomatic type class demos; wenzelm parents: diff changeset	24	use_thy "GroupDefs";
18b1441fb603 Various axiomatic type class demos; wenzelm parents: diff changeset	25	use_thy "GroupInsts";

author	wenzelm
	Tue, 24 Aug 1999 11:50:58 +0200
changeset 7333	6cb15c6f1d9f
parent 7240	a509730e424b
child 7650	c3e5e85de4c3
permissions	-rw-r--r--