| changeset 9596 | 6d6bf351b2cc |
| parent 9101 | b643f4d7b9e9 |
| child 9802 | adda1dc18bb8 |
| 9595:ec388b0a4eaa | 9596:6d6bf351b2cc |
|---|---|
15 |
15 |
16 consts |
16 consts |
17 acc :: "('a * 'a)set => 'a set" -- {* accessible part *} |
17 acc :: "('a * 'a)set => 'a set" -- {* accessible part *} |
18 |
18 |
19 inductive "acc r" |
19 inductive "acc r" |
20 intrs |
20 intros |
21 accI [rulify_prems]: |
21 accI [rulify_prems]: |
22 "ALL y. (y, x) : r --> y : acc r ==> x : acc r" |
22 "ALL y. (y, x) : r --> y : acc r ==> x : acc r" |
23 |
23 |
24 syntax |
24 syntax |
25 termi :: "('a * 'a)set => 'a set" |
25 termi :: "('a * 'a)set => 'a set" |