isabelle: src/HOL/AxClasses/Group/ROOT.ML@50ec59aff389 (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
9000 c20d58286a51 cleaned up; wenzelm parents: 7650 diff changeset	11	time_use_thy "Monoid";
c20d58286a51 cleaned up; wenzelm parents: 7650 diff changeset	12	time_use_thy "Group";
c20d58286a51 cleaned up; wenzelm parents: 7650 diff changeset	13	time_use_thy "MonoidGroupInsts";
c20d58286a51 cleaned up; wenzelm parents: 7650 diff changeset	14	time_use_thy "GroupInsts";