Now Datatype.occs_in_prems prints the necessary warning ITSELF.
It is also easier to invoke and even works if the induction variable
is a parameter (rather than a free variable).
(* Title: HOL/AxClasses/Group/ROOT.ML
ID: $Id$
Author: Markus Wenzel, TU Muenchen
Some bits of group theory via axiomatic type classes.
*)
reset HOL_quantifiers;
set show_types;
set show_sorts;
(*disable bug compatibility*)
reset force_strip_shyps;
set force_strip_shyps; (* FIXME tmp hack *)
use_thy "Sigs";
use_thy "Monoid";
use_thy "Group";
use_thy "MonoidGroupInsts";
use_thy "GroupDefs";
use_thy "GroupInsts";