doc-src/Codegen/Thy/Introduction.thy
changeset 40753 5288144b4358
parent 39745 3aa2bc9c5478
child 42096 9f6652122963
equal deleted inserted replaced
40752:aae9a020fa77 40753:5288144b4358
   212       introduced in \secref{sec:refinement}.
   212       introduced in \secref{sec:refinement}.
   213 
   213 
   214     \item Inductive predicates can be turned executable using an
   214     \item Inductive predicates can be turned executable using an
   215       extension of the code generator \secref{sec:inductive}.
   215       extension of the code generator \secref{sec:inductive}.
   216 
   216 
       
   217     \item If you want to utilize code generation to obtain fast
       
   218       evaluators e.g.~for decision procedures, have a look at
       
   219       \secref{sec:evaluation}.
       
   220 
   217     \item You may want to skim over the more technical sections
   221     \item You may want to skim over the more technical sections
   218       \secref{sec:adaptation} and \secref{sec:further}.
   222       \secref{sec:adaptation} and \secref{sec:further}.
   219 
   223 
   220     \item For exhaustive syntax diagrams etc. you should visit the
   224     \item For exhaustive syntax diagrams etc. you should visit the
   221       Isabelle/Isar Reference Manual \cite{isabelle-isar-ref}.
   225       Isabelle/Isar Reference Manual \cite{isabelle-isar-ref}.