| changeset 314 | 20a57552d722 |
| parent 311 | 8b8db9558ecf |
| child 359 | fedc16924b76 |
| 313:3b8e3a156200 | 314:20a57552d722 |
|---|---|
191 |
191 |
192 lemma ders_append: |
192 lemma ders_append: |
193 shows "ders (s1 @ s2) r = ders s2 (ders s1 r)" |
193 shows "ders (s1 @ s2) r = ders s2 (ders s1 r)" |
194 by (induct s1 arbitrary: s2 r) (auto) |
194 by (induct s1 arbitrary: s2 r) (auto) |
195 |
195 |
196 |
196 lemma ders_snoc: |
197 shows "ders (s @ [c]) r = der c (ders s r)" |
|
198 by (simp add: ders_append) |
|
197 |
199 |
198 end |
200 end |