equal
deleted
inserted
replaced
10 "imports Base \"Package/Simple_Inductive_Package\"", |
10 "imports Base \"Package/Simple_Inductive_Package\"", |
11 "begin"] |
11 "begin"] |
12 *} |
12 *} |
13 (*>*) |
13 (*>*) |
14 |
14 |
15 chapter {* Parsing *} |
15 chapter {* Parsing\label{chp:parsing} *} |
16 |
16 |
17 text {* |
17 text {* |
18 Isabelle distinguishes between \emph{outer} and \emph{inner} |
18 Isabelle distinguishes between \emph{outer} and \emph{inner} |
19 syntax. Commands, such as \isacommand{definition}, \isacommand{inductive} |
19 syntax. Commands, such as \isacommand{definition}, \isacommand{inductive} |
20 and so on, belong to the outer syntax, whereas terms, types and so on belong |
20 and so on, belong to the outer syntax, whereas terms, types and so on belong |