| changeset 16417 | 9bc16273c2d4 |
| parent 13784 | b9f6154427a4 |
| child 22710 | f44439cdce77 |
| 16416:6061ae1f90f2 | 16417:9bc16273c2d4 |
|---|---|
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: |
20 theory WF imports Trancl begin |
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)" |