From cfad21e2960b1ff8f67c1dd00aeff1c5683062b3 Mon Sep 17 00:00:00 2001 From: Burkhart Wolff Date: Sun, 14 Mar 2021 15:45:42 +0100 Subject: [PATCH] Ref auf Makarius Text added --- .../TR_MyCommentedIsabelle.thy | 10 ++++++++-- 1 file changed, 8 insertions(+), 2 deletions(-) diff --git a/examples/technical_report/TR_my_commented_isabelle/TR_MyCommentedIsabelle.thy b/examples/technical_report/TR_my_commented_isabelle/TR_MyCommentedIsabelle.thy index 4054bbd..73d7058 100755 --- a/examples/technical_report/TR_my_commented_isabelle/TR_MyCommentedIsabelle.thy +++ b/examples/technical_report/TR_my_commented_isabelle/TR_MyCommentedIsabelle.thy @@ -60,8 +60,14 @@ text\ \<^vs>\-0.5cm\ spectrum of applications. A particular strength of the Isabelle framework is the combination of text editing, formal verification, and code generation. This is a programming-tutorial of Isabelle and Isabelle/HOL, a complementary text to the unfortunately somewhat outdated - "The Isabelle Cookbook" in \<^url>\https://nms.kcl.ac.uk/christian.urban/Cookbook/\. The reader - is encouraged not only to consider the generated .pdf, but also consult the loadable version + "The Isabelle Cookbook" in \<^url>\https://nms.kcl.ac.uk/christian.urban/Cookbook/\. + The present text is also complementary to the current version of + \<^url>\https://isabelle.in.tum.de/dist/Isabelle2021/doc/isar-ref.pdf\ + "The Isabelle/Isar Implementation" by Makarius Wenzel in that it focusses on subjects + not covered there, or presents alternative explanations for which I believe, based on my + experiences with students and Phds, that they are helpful. + For the present programming manual, the reader is encouraged not only to consider the generated + .pdf, but also consult the loadable version in Isabelle/jedit in order to make experiments on the running code. This text is written itself in Isabelle/Isar using a specific document ontology for technical reports. It is intended to be a "living document", i.e. it is not only used for generating a static,