changeset 16417 | 9bc16273c2d4 |
parent 15481 | fc075ae929e4 |
child 23767 | 7272a839ccd9 |
16416:6061ae1f90f2 | 16417:9bc16273c2d4 |
---|---|
13 Based on Lex/Prefix |
13 Based on Lex/Prefix |
14 *) |
14 *) |
15 |
15 |
16 header {*The Prefix Ordering on Lists*} |
16 header {*The Prefix Ordering on Lists*} |
17 |
17 |
18 theory ListOrder = Main: |
18 theory ListOrder imports Main begin |
19 |
19 |
20 consts |
20 consts |
21 genPrefix :: "('a * 'a)set => ('a list * 'a list)set" |
21 genPrefix :: "('a * 'a)set => ('a list * 'a list)set" |
22 |
22 |
23 inductive "genPrefix(r)" |
23 inductive "genPrefix(r)" |