equal
deleted
inserted
replaced
9 text \<open> |
9 text \<open> |
10 The code generator is actually a framework consisting of different |
10 The code generator is actually a framework consisting of different |
11 components which can be customised individually. |
11 components which can be customised individually. |
12 |
12 |
13 Conceptually all components operate on Isabelle's logic framework |
13 Conceptually all components operate on Isabelle's logic framework |
14 @{theory Pure}. Practically, the object logic @{theory HOL} |
14 Pure. Practically, the object logic HOL |
15 provides the necessary facilities to make use of the code generator, |
15 provides the necessary facilities to make use of the code generator, |
16 mainly since it is an extension of @{theory Pure}. |
16 mainly since it is an extension of Isabelle/Pure. |
17 |
17 |
18 The constellation of the different components is visualized in the |
18 The constellation of the different components is visualized in the |
19 following picture. |
19 following picture. |
20 |
20 |
21 \begin{figure}[h] |
21 \begin{figure}[h] |