| changeset 272 | 1446bc47a294 |
| parent 227 | 93bd75031ced |
| child 355 | a259eec25156 |
| 271:b9b54574ee41 | 272:1446bc47a294 |
|---|---|
301 lemma matcher_correctness: |
301 lemma matcher_correctness: |
302 shows "matcher r s \<longleftrightarrow> s \<in> L r" |
302 shows "matcher r s \<longleftrightarrow> s \<in> L r" |
303 by (induct s arbitrary: r) |
303 by (induct s arbitrary: r) |
304 (simp_all add: nullable_correctness der_correctness Der_def) |
304 (simp_all add: nullable_correctness der_correctness Der_def) |
305 |
305 |
306 ` |
306 |
307 end |
307 end |