src/HOL/AxClasses/Tutorial/Group.ML
changeset 5711 5a1cd4b4b20e
parent 5069 3ea049f7979d
equal deleted inserted replaced
5710:30f4d3713cbe 5711:5a1cd4b4b20e
     2     ID:         $Id$
     2     ID:         $Id$
     3     Author:     Markus Wenzel, TU Muenchen
     3     Author:     Markus Wenzel, TU Muenchen
     4 
     4 
     5 Some basic theorems of group theory.
     5 Some basic theorems of group theory.
     6 *)
     6 *)
     7 
       
     8 open Group;
       
     9 
     7 
    10 fun sub r = standard (r RS subst);
     8 fun sub r = standard (r RS subst);
    11 fun ssub r = standard (r RS ssubst);
     9 fun ssub r = standard (r RS ssubst);
    12 
    10 
    13 
    11