equal
deleted
inserted
replaced
1 theory Outer_Syntax |
1 theory Outer_Syntax |
2 imports Base Main |
2 imports Base Main |
3 begin |
3 begin |
4 |
4 |
5 chapter {* Outer syntax *} |
5 chapter {* Outer syntax --- the theory language *} |
6 |
6 |
7 text {* |
7 text {* |
8 The rather generic framework of Isabelle/Isar syntax emerges from |
8 The rather generic framework of Isabelle/Isar syntax emerges from |
9 three main syntactic categories: \emph{commands} of the top-level |
9 three main syntactic categories: \emph{commands} of the top-level |
10 Isar engine (covering theory and proof elements), \emph{methods} for |
10 Isar engine (covering theory and proof elements), \emph{methods} for |