equal
deleted
inserted
replaced
19 acc :: "('a * 'a)set => 'a set" (*Accessible part*) |
19 acc :: "('a * 'a)set => 'a set" (*Accessible part*) |
20 |
20 |
21 inductive "acc(r)" |
21 inductive "acc(r)" |
22 intrs |
22 intrs |
23 pred "pred a r: Pow(acc(r)) ==> a: acc(r)" |
23 pred "pred a r: Pow(acc(r)) ==> a: acc(r)" |
24 monos "[Pow_mono]" |
24 monos Pow_mono |
25 |
25 |
26 syntax termi :: "('a * 'a)set => 'a set" |
26 syntax termi :: "('a * 'a)set => 'a set" |
27 translations "termi r" == "acc(r^-1)" |
27 translations "termi r" == "acc(r^-1)" |
28 |
28 |
29 end |
29 end |