From 2e645ed5ff06178f538cc34adee104ca9656ce73 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Nicolas=20M=C3=A9ric?= Date: Thu, 3 Feb 2022 11:33:56 +0100 Subject: [PATCH] Update structure of Advanced Evaluation section --- examples/scholarly_paper/2021-ITP-PMTI/paper.thy | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/examples/scholarly_paper/2021-ITP-PMTI/paper.thy b/examples/scholarly_paper/2021-ITP-PMTI/paper.thy index f3e759c..b7ac953 100644 --- a/examples/scholarly_paper/2021-ITP-PMTI/paper.thy +++ b/examples/scholarly_paper/2021-ITP-PMTI/paper.thy @@ -422,8 +422,9 @@ subsection\Advanced Evaluation in Isabelle\ text\Besides the powerful, but relatively slow rewriting-based proof method \<^theory_text>\simp\, there are basically two other techniques for the evaluation of terms: \<^item> evaluation via reflection into SML (\<^theory_text>\eval\), and -\<^item> normalization by evaluation @{cite "AehligHN12"} (\<^theory_text>\nbe\). +\<^item> normalization by evaluation @{cite "AehligHN12"} (\<^theory_text>\nbe\).\ +text\ 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