| changeset 647 | 70c10dc41606 |
| parent 642 | 6c13f76c070b |
| 646:56057198e4f5 | 647:70c10dc41606 |
|---|---|
1 theory LexerSimp |
1 theory LexerSimp |
2 imports "Lexer" |
2 imports "Lexer" |
3 begin |
3 begin |
4 |
4 |
5 section {* Lexer including some simplifications *} |
5 section \<open>Lexer including some simplifications\<close> |
6 |
6 |
7 |
7 |
8 fun F_RIGHT where |
8 fun F_RIGHT where |
9 "F_RIGHT f v = Right (f v)" |
9 "F_RIGHT f v = Right (f v)" |
10 |
10 |