equal
deleted
inserted
replaced
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 intrs |
21 accI [rulify_prems]: "ALL y. (y, x) : r --> y : acc r ==> x : acc r" |
21 accI [rulify_prems]: |
|
22 "ALL y. (y, x) : r --> y : acc r ==> x : acc r" |
22 |
23 |
23 |
24 syntax |
24 syntax termi :: "('a * 'a)set => 'a set" |
25 termi :: "('a * 'a)set => 'a set" |
25 translations "termi r" == "acc(r^-1)" |
26 translations |
|
27 "termi r" == "acc(r^-1)" |
26 |
28 |
27 end |
29 end |