equal
deleted
inserted
replaced
462 |
462 |
463 subsection {* Accessible Part *} |
463 subsection {* Accessible Part *} |
464 |
464 |
465 text {* |
465 text {* |
466 Inductive definition of the accessible part @{term "acc r"} of a |
466 Inductive definition of the accessible part @{term "acc r"} of a |
467 relation; see also \cite{paulin-tlca}. |
467 relation; see also @{cite "paulin-tlca"}. |
468 *} |
468 *} |
469 |
469 |
470 inductive_set |
470 inductive_set |
471 acc :: "('a * 'a) set => 'a set" |
471 acc :: "('a * 'a) set => 'a set" |
472 for r :: "('a * 'a) set" |
472 for r :: "('a * 'a) set" |