src/HOL/AxClasses/Group/ROOT.ML
author wenzelm
Sat, 30 Oct 1999 20:20:48 +0200
changeset 7982 d534b897ce39
parent 7650 c3e5e85de4c3
child 9000 c20d58286a51
permissions -rw-r--r--
improved presentation;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
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";