src/HOL/Induct/Acc.thy

 
 See Ch. Paulin-Mohring, Inductive Definitions in the System Coq.
 Research Report 92-49, LIP, ENS Lyon.  Dec 1992.
 *)
 
-header {* The accessible part of a relation *};
+header {* The accessible part of a relation *}
 
-theory Acc = WF + Inductive:;
+theory Acc = Main:
 
 consts
-  acc  :: "('a * 'a)set => 'a set"  -- {* accessible part *};
+  acc  :: "('a * 'a)set => 'a set"  -- {* accessible part *}
 
 inductive "acc r"
   intrs
     accI [rulify_prems]:
       "ALL y. (y, x) : r --> y : acc r ==> x : acc r"