|
28213
|
1 |
theory Program
|
|
|
2 |
imports Setup
|
|
|
3 |
begin
|
|
|
4 |
|
|
|
5 |
section {* Turning Theories into Programs *}
|
|
|
6 |
|
|
|
7 |
subsection {* The @{text "Isabelle/HOL"} default setup *}
|
|
|
8 |
|
|
|
9 |
text {* Invoking the code generator *}
|
|
|
10 |
|
|
|
11 |
subsection {* Selecting code equations *}
|
|
|
12 |
|
|
|
13 |
text {* inspection by @{text "code_thms"} *}
|
|
|
14 |
|
|
|
15 |
subsection {* The preprocessor *}
|
|
|
16 |
|
|
|
17 |
subsection {* Datatypes *}
|
|
|
18 |
|
|
|
19 |
text {* example: @{text "rat"}, cases *}
|
|
|
20 |
|
|
|
21 |
subsection {* Equality and wellsortedness *}
|
|
|
22 |
|
|
|
23 |
subsection {* Partiality *}
|
|
|
24 |
|
|
|
25 |
text {* @{text "code_abort"}, examples: maps *}
|
|
|
26 |
|
|
|
27 |
end
|