equal
deleted
inserted
replaced
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 |