Isabelle_DOF
/
Isabelle_DOF
1
0
Fork 2
Code Issues 1 Pull Requests Releases Wiki Activity

Update structure of Advanced Evaluation section

This commit is contained in:
Nicolas Méric 2022-02-03 11:33:56 +01:00
parent 092d552ef8
commit 2e645ed5ff
1 changed files with 2 additions and 1 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

3
examples/scholarly_paper/2021-ITP-PMTI/paper.thy
View File

@ -422,8 +422,9 @@ subsection\<open>Advanced Evaluation in Isabelle\<close>
text\<open>Besides the powerful, but relatively slow rewriting-based proof method
\<^theory_text>\<open>simp\<close>, there are basically two other techniques for the evaluation of terms:
\<^item> evaluation via reflection into SML (\<^theory_text>\<open>eval\<close>), and
\<^item> normalization by evaluation @{cite "AehligHN12"} (\<^theory_text>\<open>nbe\<close>).
\<^item> normalization by evaluation @{cite "AehligHN12"} (\<^theory_text>\<open>nbe\<close>).\<close>
text\<open>
The former is based on a nearly one-to-one compilation of datatype specification
constructs and recursive function definitions into SML datatypes and functions.
The generated code is directly compiled by the underlying SML compiler of the