| changeset 753 | ec86863e87c8 |
| parent 515 | abcc438e7c27 |
| child 810 | 91c68f74f458 |
| 752:b89462f9d5f1 | 753:ec86863e87c8 |
|---|---|
69 (*Misc definitions*) |
69 (*Misc definitions*) |
70 consts |
70 consts |
71 diamond :: "i => o" |
71 diamond :: "i => o" |
72 I :: "i" |
72 I :: "i" |
73 |
73 |
74 rules |
74 defs |
75 |
75 |
76 diamond_def "diamond(r) == ALL x y. <x,y>:r --> \ |
76 diamond_def "diamond(r) == ALL x y. <x,y>:r --> \ |
77 \ (ALL y'. <x,y'>:r --> \ |
77 \ (ALL y'. <x,y'>:r --> \ |
78 \ (EX z. <y,z>:r & <y',z> : r))" |
78 \ (EX z. <y,z>:r & <y',z> : r))" |
79 |
79 |