|
28213
|
1 |
theory Introduction
|
|
|
2 |
imports Setup
|
|
|
3 |
begin
|
|
|
4 |
|
|
|
5 |
chapter {* Code generation from @{text "Isabelle/HOL"} theories *}
|
|
|
6 |
|
|
|
7 |
section {* Introduction and Overview *}
|
|
|
8 |
|
|
|
9 |
text {*
|
|
|
10 |
This tutorial introduces a generic code generator for the
|
|
|
11 |
Isabelle system \cite{isa-tutorial}.
|
|
|
12 |
*}
|
|
|
13 |
|
|
|
14 |
subsection {* Code generation via shallow embedding *}
|
|
|
15 |
|
|
|
16 |
text {* example *}
|
|
|
17 |
|
|
|
18 |
subsection {* Code generator architecture *}
|
|
|
19 |
|
|
|
20 |
text {* foundation, forward references for yet unexplained things *}
|
|
|
21 |
|
|
|
22 |
end
|