src/HOL/Induct/Acc.thy
changeset 9101 b643f4d7b9e9
parent 7867 2efb66472812
child 9596 6d6bf351b2cc
     1.1 --- a/src/HOL/Induct/Acc.thy	Wed Jun 21 15:58:23 2000 +0200
     1.2 +++ b/src/HOL/Induct/Acc.thy	Wed Jun 21 18:09:09 2000 +0200
     1.3 @@ -9,12 +9,12 @@
     1.4  Research Report 92-49, LIP, ENS Lyon.  Dec 1992.
     1.5  *)
     1.6  
     1.7 -header {* The accessible part of a relation *};
     1.8 +header {* The accessible part of a relation *}
     1.9  
    1.10 -theory Acc = WF + Inductive:;
    1.11 +theory Acc = Main:
    1.12  
    1.13  consts
    1.14 -  acc  :: "('a * 'a)set => 'a set"  -- {* accessible part *};
    1.15 +  acc  :: "('a * 'a)set => 'a set"  -- {* accessible part *}
    1.16  
    1.17  inductive "acc r"
    1.18    intrs