| changeset 198 | f54972b0f641 |
| parent 196 | 7182786d9c68 |
| child 227 | 93bd75031ced |
| 197:6622bd256029 | 198:f54972b0f641 |
|---|---|
297 lemma matcher_correctness: |
297 lemma matcher_correctness: |
298 shows "matcher r s \<longleftrightarrow> s \<in> L r" |
298 shows "matcher r s \<longleftrightarrow> s \<in> L r" |
299 by (induct s arbitrary: r) |
299 by (induct s arbitrary: r) |
300 (simp_all add: nullable_correctness der_correctness Der_def) |
300 (simp_all add: nullable_correctness der_correctness Der_def) |
301 |
301 |
302 |
302 ` |
303 end |
303 end |