src/HOL/Library/Accessible_Part.thy
changeset 15131 c69542757a4d
parent 14706 71590b7733b7
child 15140 322485b816ac
equal deleted inserted replaced
15130:dc6be28d7f4e 15131:c69542757a4d
     4     Copyright   1994  University of Cambridge
     4     Copyright   1994  University of Cambridge
     5 *)
     5 *)
     6 
     6 
     7 header {* The accessible part of a relation *}
     7 header {* The accessible part of a relation *}
     8 
     8 
     9 theory Accessible_Part = Main:
     9 theory Accessible_Part
    10 
    10 import Main
       
    11 begin
    11 
    12 
    12 subsection {* Inductive definition *}
    13 subsection {* Inductive definition *}
    13 
    14 
    14 text {*
    15 text {*
    15  Inductive definition of the accessible part @{term "acc r"} of a
    16  Inductive definition of the accessible part @{term "acc r"} of a