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

Documented component registration.

This commit is contained in:
Achim D. Brucker 2022-06-29 18:50:44 +01:00
parent 367d8f28ad
commit 909dda1ea2
1 changed files with 7 additions and 3 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

10
examples/technical_report/Isabelle_DOF-Manual/03_GuidedTour.thy
View File

@ -75,16 +75,20 @@ text\<open>
@{boxed_bash [display]\<open>ë\prompt{}ë tar xf ë\href{\isadofarchiveurl}{\isadofarchiven}ë\<close>}
This will create a directory \texttt{\isadofdirn} containing \<^isadof> distribution.
\<^isadof> depends on the the AFP (\<^url>\<open>https://www.isa-afp.org\<close>), namely the AFP
Next, we need to register \<^isadof> as an Isabelle component:
@{boxed_bash [display]\<open>ë\prompt{}ë isabelle components -u ë\mbox{\isadofdirn}ë\<close>}
Moreover, \<^isadof> depends on the the AFP (\<^url>\<open>https://www.isa-afp.org\<close>), 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>\<open>https://www.isa-afp.org/using.html\<close>),
or use the provided \<^boxed_bash>\<open>install\<close> script to install a minimal AFP
setup into the local \<^isadof> directory. The script needs to be prefixed with the
\<^boxed_bash>\<open>isabelle env\<close> command:
\<^boxed_bash>\<open>isabelle eëënv\<close> command:
@{boxed_bash [display]\<open>ë\prompt{}ë cd ë\isadofdirnë
ë\prompt{\isadofdirn}ë isabelle env ./install-afp
ë\prompt{\isadofdirn}ë isabelle eëënv ë\mbox{./install-afp}ë
Isabelle/DOF Installer
======================