From 8722b21c3d81a3b8cd47741c75259184a7143c4a Mon Sep 17 00:00:00 2001
From: Burkhart Wolff <wolff@lri.fr>
Date: Wed, 13 Apr 2022 12:11:44 +0200
Subject: [PATCH] shortened para 2.3

- added ref on eval
- reduced blur
- fused 3 paras into one by avoiding
  in-depth explication of the techniques
- established link to runtime-testing and the title
---
 .../2021-ITP-PMTI/document/root.bib           | 22 +++++++++++++++++++
 .../scholarly_paper/2021-ITP-PMTI/paper.thy   | 21 ++++++++++++------
 2 files changed, 36 insertions(+), 7 deletions(-)

diff --git a/examples/scholarly_paper/2021-ITP-PMTI/document/root.bib b/examples/scholarly_paper/2021-ITP-PMTI/document/root.bib
index 1ee3b370..a3c981ad 100644
--- a/examples/scholarly_paper/2021-ITP-PMTI/document/root.bib
+++ b/examples/scholarly_paper/2021-ITP-PMTI/document/root.bib
@@ -174,6 +174,28 @@ isbn="978-3-030-79876-5"
   year={1998},
   organization={Springer}
 }
+
+
+@inproceedings{HaftmannN10,
+  author    = {Florian Haftmann and
+               Tobias Nipkow},
+  editor    = {Matthias Blume and
+               Naoki Kobayashi and
+               Germ{\'{a}}n Vidal},
+  title     = {Code Generation via Higher-Order Rewrite Systems},
+  booktitle = {Functional and Logic Programming, 10th International Symposium, {FLOPS}
+               2010, Sendai, Japan, April 19-21, 2010. Proceedings},
+  series    = {Lecture Notes in Computer Science},
+  volume    = {6009},
+  pages     = {103--117},
+  publisher = {Springer},
+  year      = {2010},
+  url       = {https://doi.org/10.1007/978-3-642-12251-4\_9},
+  doi       = {10.1007/978-3-642-12251-4\_9},
+  timestamp = {Wed, 25 Sep 2019 18:04:25 +0200},
+  biburl    = {https://dblp.org/rec/conf/flops/HaftmannN10.bib},
+  bibsource = {dblp computer science bibliography, https://dblp.org}
+}
                     
 @article{AehligHN12,
   author    = {Klaus Aehlig and
diff --git a/examples/scholarly_paper/2021-ITP-PMTI/paper.thy b/examples/scholarly_paper/2021-ITP-PMTI/paper.thy
index 8ee80dfe..559bab2d 100644
--- a/examples/scholarly_paper/2021-ITP-PMTI/paper.thy
+++ b/examples/scholarly_paper/2021-ITP-PMTI/paper.thy
@@ -406,15 +406,22 @@ types and can therefore be inherited in a subclass.
 \<close>
 
 
-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
+subsection\<open>Term-Evaluations in Isabelle\<close>
+text\<open>Besides the powerful, but relatively slow Isabelle rewriting-based proof method,
+ there are  two other techniques for term evaluation:
+\<^item> evaluation via reflection @{cite "HaftmannN10"} (\<^theory_text>\<open>eval\<close>), and
 \<^item> normalization by evaluation @{cite "AehligHN12"} (\<^theory_text>\<open>nbe\<close>).\<close>
 
+text\<open> \<^noindent>  The former is based on a nearly one-to-one compilation of HOL-level datatype specifications 
+and function definitions into SML datatypes and functions.
+The latter technique --- enabling free variables in terms --- uses a generic data-universe
+enriched by explicit variables. Both techniques are several orders of magnitude more efficient 
+than standard rewriting. \<^dof> uses both to generate code that evaluates invariant and data-integrity 
+checks on-the-fly during editing. For all examples in our library, this form of runtime-testing
+ is sufficiently fast to remain unnoticed by the user.
+\<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 
 Isabelle platform. This way, pattern-matching becomes natively compiled rather
 than interpreted as in the matching process of \<^theory_text>\<open>simp\<close>. @{cite "AehligHN12"} 
@@ -433,7 +440,7 @@ for ontological classes on the fly during editing, paving the way for both
 a uniform specification language of ontological data --- namely \<^hol> --- as
 well as the possibility to \<^emph>\<open>prove\<close> properties over and relations between
 classes.\<close>
-
+*)
 
 section*[invariants::technical,main_author="Some(@{docitem ''nic''}::author)"] 
 \<open>Term-Context Support, Invariants and Queries in DOF\<close>