doc-src/IsarAdvanced/Codegen/Thy/Introduction.thy

New outline for codegen tutorial -- draft

theory Introduction
imports Setup
begin

chapter {* Code generation from @{text "Isabelle/HOL"} theories *}

section {* Introduction and Overview *}

text {*
  This tutorial introduces a generic code generator for the
  Isabelle system \cite{isa-tutorial}.
*}

subsection {* Code generation via shallow embedding *}

text {* example *}

subsection {* Code generator architecture *}

text {* foundation, forward references for yet unexplained things  *}

end