| changeset 290 | 6e1c03614d36 |
| parent 288 | a9003e6d0463 |
| child 291 | 93db7414931d |
| 289:4e50ff177348 | 290:6e1c03614d36 |
|---|---|
2792 thus "?thesis" |
2792 thus "?thesis" |
2793 using compile |
2793 using compile |
2794 using wf_tm_from_abacus[of "tm_of (a [+] dummy_abc b)" "(a [+] dummy_abc b)" b] |
2794 using wf_tm_from_abacus[of "tm_of (a [+] dummy_abc b)" "(a [+] dummy_abc b)" b] |
2795 by simp |
2795 by simp |
2796 qed |
2796 qed |
2797 |
2797 |
2798 unused_thms |
|
2799 |
|
2798 end |
2800 end |