src/HOL/AxClasses/Tutorial/ROOT.ML
author nipkow
Mon Oct 21 09:50:50 1996 +0200 (1996-10-21)
changeset 2115 9709f9188549
parent 1572 dbecd983863f
child 7240 a509730e424b
permissions -rw-r--r--
Added trans_tac (see Provers/nat_transitive.ML)
     1 (*  Title:      HOL/AxClasses/Tutorial/ROOT.ML
     2     ID:         $Id$
     3     Author:     Markus Wenzel, TU Muenchen
     4 
     5 Some simple axclass demos that go along with the paper "Using
     6 Axiomatic Type Classes in Isabelle --- a tutorial".  (The NatClass
     7 example resides in directory FOL/ex/.)
     8 *)
     9 
    10 reset HOL_quantifiers;
    11 set show_types;
    12 set show_sorts;
    13 
    14 
    15 (* Semigroups *)
    16 
    17 use_thy "Semigroup";
    18 use_thy "Semigroups";
    19 
    20 
    21 (* Basic group theory *)
    22 
    23 use_thy "Sigs";
    24 use_thy "Monoid";
    25 use_thy "Group";
    26 use_thy "MonoidGroupInsts";
    27 use_thy "Xor";
    28 use_thy "BoolGroupInsts";
    29 use_thy "ProdGroupInsts";
    30 
    31 
    32 (* Syntactic classes *)
    33 
    34 use_thy "Product";
    35 use_thy "ProductInsts";