equal
deleted
inserted
replaced
4 |
4 |
5 (*<*) |
5 (*<*) |
6 setup{* |
6 setup{* |
7 open_file_with_prelude |
7 open_file_with_prelude |
8 "Advanced_Code.thy" |
8 "Advanced_Code.thy" |
9 ["theory General", "imports Base FirstSteps", "begin"] |
9 ["theory Advanced", "imports Base FirstSteps", "begin"] |
10 *} |
10 *} |
11 (*>*) |
11 (*>*) |
12 |
12 |
13 |
13 |
14 chapter {* Advanced Isabelle *} |
14 chapter {* Advanced Isabelle *} |
27 *} |
27 *} |
28 |
28 |
29 section {* Theories\label{sec:theories} (TBD) *} |
29 section {* Theories\label{sec:theories} (TBD) *} |
30 |
30 |
31 text {* |
31 text {* |
32 As said above, theories are the most basic layer in Isabelle. They contain |
32 Theories, as said above, are the most basic layer in Isabelle. They contain |
33 definitions, syntax declarations, axioms, proofs etc. If a definition is |
33 definitions, syntax declarations, axioms, proofs etc. If a definition is |
34 stated, it must be stored in a theory in order to be usable later |
34 stated, it must be stored in a theory in order to be usable later |
35 on. Similar with proofs: once a proof is finished, the proved theorem needs |
35 on. Similar with proofs: once a proof is finished, the proved theorem needs |
36 to be stored in the theorem database of the theory in order to be |
36 to be stored in the theorem database of the theory in order to be |
37 usable. All relevant data of a theory can be queried as follows. |
37 usable. All relevant data of a theory can be queried as follows. |