equal
deleted
inserted
replaced
228 ultimately show "slexer r (c # s) = lexer r (c # s)" |
228 ultimately show "slexer r (c # s) = lexer r (c # s)" |
229 by (simp del: slexer.simps add: slexer_better_simp) |
229 by (simp del: slexer.simps add: slexer_better_simp) |
230 qed |
230 qed |
231 qed |
231 qed |
232 |
232 |
233 |
233 (* |
234 fun simp2_ALT where |
234 fun simp2_ALT where |
235 "simp2_ALT ZERO r2 seen = (r2, seen)" |
235 "simp2_ALT ZERO r2 seen = (r2, seen)" |
236 | "simp2_ALT r1 ZERO seen = (r1, seen)" |
236 | "simp2_ALT r1 ZERO seen = (r1, seen)" |
237 | "simp2_ALT r1 r2 seen = (ALT r1 r2, seen)" |
237 | "simp2_ALT r1 r2 seen = (ALT r1 r2, seen)" |
238 |
238 |
365 using L.simps(3) apply blast |
365 using L.simps(3) apply blast |
366 prefer 2 |
366 prefer 2 |
367 apply(simp add: Sequ_def) |
367 apply(simp add: Sequ_def) |
368 apply(auto)[1] |
368 apply(auto)[1] |
369 oops |
369 oops |
370 |
370 *) |
371 end |
371 end |