equal
deleted
inserted
replaced
169 by (induct s arbitrary: r) |
169 by (induct s arbitrary: r) |
170 (simp_all add: nullable_correctness der_correctness Der_def) |
170 (simp_all add: nullable_correctness der_correctness Der_def) |
171 |
171 |
172 section {* Examples *} |
172 section {* Examples *} |
173 |
173 |
|
174 definition |
|
175 "CHRA \<equiv> CHAR (CHR ''a'')" |
|
176 |
|
177 definition |
|
178 "ALT1 \<equiv> ALT CHRA EMPTY" |
|
179 |
|
180 definition |
|
181 "SEQ3 \<equiv> SEQ (SEQ ALT1 ALT1) ALT1" |
|
182 |
|
183 value "matcher SEQ3 ''aaa''" |
|
184 |
174 value "matcher NULL []" |
185 value "matcher NULL []" |
175 value "matcher (CHAR (CHR ''a'')) [CHR ''a'']" |
186 value "matcher (CHAR (CHR ''a'')) [CHR ''a'']" |
176 value "matcher (CHAR a) [a,a]" |
187 value "matcher (CHAR a) [a,a]" |
177 value "matcher (STAR (CHAR a)) []" |
188 value "matcher (STAR (CHAR a)) []" |
178 value "matcher (STAR (CHAR a)) [a,a]" |
189 value "matcher (STAR (CHAR a)) [a,a]" |