*** empty log message ***
authorwenzelm
Mon, 15 Jan 1996 15:50:54 +0100
changeset 1442 7a8a30b11a24
parent 1441 7fbe815c18ad
child 1443 ff8a804e0201
*** empty log message ***
src/HOL/AxClasses/Group/ROOT.ML
--- a/src/HOL/AxClasses/Group/ROOT.ML	Mon Jan 15 15:50:41 1996 +0100
+++ b/src/HOL/AxClasses/Group/ROOT.ML	Mon Jan 15 15:50:54 1996 +0100
@@ -2,8 +2,7 @@
     ID:         $Id$
     Author:     Markus Wenzel, TU Muenchen
 
-(* FIXME comment *)
-Elementary algebra via axiomatic type classes.
+Some bits of group theory via axiomatic type classes.
 *)
 
 reset HOL_quantifiers;
@@ -13,7 +12,7 @@
 (*disable bug compatibility*)
 reset force_strip_shyps;
 
-set force_strip_shyps;(* FIXME tmp hack *)
+set force_strip_shyps; (* FIXME tmp hack *)
 
 
 use_thy "Sigs";