| changeset 13357 | 6f54e992777e |
| parent 13356 | c9cfe1638bf2 |
| child 13534 | ca6debb89d77 |
| 13356:c9cfe1638bf2 | 13357:6f54e992777e |
|---|---|
15 a mess. |
15 a mess. |
16 *) |
16 *) |
17 |
17 |
18 header{*Well-Founded Recursion*} |
18 header{*Well-Founded Recursion*} |
19 |
19 |
20 theory WF = Trancl + mono + equalities: |
20 theory WF = Trancl: |
21 |
21 |
22 constdefs |
22 constdefs |
23 wf :: "i=>o" |
23 wf :: "i=>o" |
24 (*r is a well-founded relation*) |
24 (*r is a well-founded relation*) |
25 "wf(r) == ALL Z. Z=0 | (EX x:Z. ALL y. <y,x>:r --> ~ y:Z)" |
25 "wf(r) == ALL Z. Z=0 | (EX x:Z. ALL y. <y,x>:r --> ~ y:Z)" |