isabelle: src/HOL/AxClasses/Group/ROOT.ML@c3e5e85de4c3 (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	use_thy "Monoid";
18b1441fb603 Various axiomatic type class demos; wenzelm parents: diff changeset	12	use_thy "Group";
18b1441fb603 Various axiomatic type class demos; wenzelm parents: diff changeset	13	use_thy "MonoidGroupInsts";
18b1441fb603 Various axiomatic type class demos; wenzelm parents: diff changeset	14	use_thy "GroupInsts";