tuned presentation;

--- a/src/HOL/Induct/Acc.thy	Wed Oct 06 18:14:26 1999 +0200
+++ b/src/HOL/Induct/Acc.thy	Wed Oct 06 18:15:22 1999 +0200
@@ -9,10 +9,12 @@
 Research Report 92-49, LIP, ENS Lyon.  Dec 1992.
 *)
 
-theory Acc = WF + Inductive:
+header {* The acessible part of a relation *};
+
+theory Acc = WF + Inductive:;
 
 consts
-  acc  :: "('a * 'a)set => 'a set"              (*Accessible part*)
+  acc  :: "('a * 'a)set => 'a set"  -- {* accessible part *};
 
 inductive "acc r"
   intrs