From 909dda1ea2f9c3c46bf6ff125b1730b4e3339481 Mon Sep 17 00:00:00 2001 From: "Achim D. Brucker" Date: Wed, 29 Jun 2022 18:50:44 +0100 Subject: [PATCH] Documented component registration. --- .../Isabelle_DOF-Manual/03_GuidedTour.thy | 10 +++++++--- 1 file changed, 7 insertions(+), 3 deletions(-) diff --git a/examples/technical_report/Isabelle_DOF-Manual/03_GuidedTour.thy b/examples/technical_report/Isabelle_DOF-Manual/03_GuidedTour.thy index ac47351..1e6ff39 100644 --- a/examples/technical_report/Isabelle_DOF-Manual/03_GuidedTour.thy +++ b/examples/technical_report/Isabelle_DOF-Manual/03_GuidedTour.thy @@ -75,16 +75,20 @@ text\ @{boxed_bash [display]\ë\prompt{}ë tar xf ë\href{\isadofarchiveurl}{\isadofarchiven}ë\} This will create a directory \texttt{\isadofdirn} containing \<^isadof> distribution. -\<^isadof> depends on the the AFP (\<^url>\https://www.isa-afp.org\), namely the AFP +Next, we need to register \<^isadof> as an Isabelle component: + +@{boxed_bash [display]\ë\prompt{}ë isabelle components -u ë\mbox{\isadofdirn}ë\} + +Moreover, \<^isadof> depends on the the AFP (\<^url>\https://www.isa-afp.org\), namely the AFP entries ``Functional Automata''~@{cite "nipkow.ea:functional-Automata-afp:2004"} and ``Regular Sets and Expressions''~@{cite "kraus.ea:regular-sets-afp:2010"}. You can either install the complete AFP, following the instructions given at \<^url>\https://www.isa-afp.org/using.html\), or use the provided \<^boxed_bash>\install\ script to install a minimal AFP setup into the local \<^isadof> directory. The script needs to be prefixed with the -\<^boxed_bash>\isabelle env\ command: +\<^boxed_bash>\isabelle eëënv\ command: @{boxed_bash [display]\ë\prompt{}ë cd ë\isadofdirnë -ë\prompt{\isadofdirn}ë isabelle env ./install-afp +ë\prompt{\isadofdirn}ë isabelle eëënv ë\mbox{./install-afp}ë Isabelle/DOF Installer ======================