| changeset 642 | 6c13f76c070b |
| parent 495 | f9cdc295ccf7 |
| 641:cf7a5c863831 | 642:6c13f76c070b |
|---|---|
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 |