# HG changeset patch
# User wenzelm
# Date 939226522 -7200
# Node ID 44dd5dc8e90fb5b8d3d202ac4862791892649668
# Parent  d36c19045493efcd62c20b7cc39e5fdd9acc3e7e
tuned presentation;

diff -r d36c19045493 -r 44dd5dc8e90f src/HOL/Induct/Acc.thy
--- 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