equal
deleted
inserted
replaced
1 theory Parsing |
1 theory Parsing |
2 imports Base "Helper/Command/Command" "Package/Simple_Inductive_Package" |
2 imports Base "Helper/Command/Command" "Package/Simple_Inductive_Package" |
3 uses "Parsing.ML" |
|
4 begin |
3 begin |
|
4 |
|
5 (*<*) |
|
6 setup {* |
|
7 open_file_with_prelude |
|
8 "Parsing_Code.thy" |
|
9 ["theory Parsing", |
|
10 "imports Base \"Package/Simple_Inductive_Package\"", |
|
11 "begin"] |
|
12 *} |
|
13 (*>*) |
5 |
14 |
6 chapter {* Parsing *} |
15 chapter {* Parsing *} |
7 |
16 |
8 text {* |
17 text {* |
9 Isabelle distinguishes between \emph{outer} and \emph{inner} |
18 Isabelle distinguishes between \emph{outer} and \emph{inner} |