equal
deleted
inserted
replaced
1 |
1 |
2 header {* Example: First-Order Logic *} |
2 header {* Example: First-Order Logic *} |
3 |
3 |
4 theory %visible First_Order_Logic |
4 theory %visible First_Order_Logic |
5 imports Pure |
5 imports Base (* FIXME Pure!? *) |
6 begin |
6 begin |
7 |
7 |
8 text {* |
8 text {* |
9 \noindent In order to commence a new object-logic within |
9 \noindent In order to commence a new object-logic within |
10 Isabelle/Pure we introduce abstract syntactic categories @{text "i"} |
10 Isabelle/Pure we introduce abstract syntactic categories @{text "i"} |