| changeset 2409 | 83990a42a068 |
| parent 2407 | 49ab06c0ca64 |
| child 2410 | 2bbdb9c427b5 |
| 2408:f1980f89c405 | 2409:83990a42a068 |
|---|---|
19 binder |
19 binder |
20 bn::"assg \<Rightarrow> atom set" |
20 bn::"assg \<Rightarrow> atom set" |
21 where |
21 where |
22 "bn (As x y t) = {atom x}" |
22 "bn (As x y t) = {atom x}" |
23 |
23 |
24 (* can lift *) |
24 ML {* Function.prove_termination *} |
25 |
|
26 text {* can lift *} |
|
25 |
27 |
26 thm distinct |
28 thm distinct |
27 thm trm_raw_assg_raw.inducts |
29 thm trm_raw_assg_raw.inducts |
28 thm trm_raw.exhaust |
30 thm trm_raw.exhaust |
29 thm assg_raw.exhaust |
31 thm assg_raw.exhaust |