Cleanup.
|
@ -29,24 +29,17 @@ session "Isabelle_DOF" (AFP) = "Functional-Automata" +
|
|||
"root.mst"
|
||||
"preamble.tex"
|
||||
"lstisadof-manual.sty"
|
||||
"figures/antiquotations-PIDE.png"
|
||||
"figures/cicm2018-combined.png"
|
||||
"figures/cicm2018-dof.png"
|
||||
"figures/cicm2018-pdf.png"
|
||||
"figures/document-hierarchy.pdf"
|
||||
"figures/document-hierarchy.svg"
|
||||
"figures/Dogfood-figures.png"
|
||||
"figures/Dogfood-II-bgnd1.png"
|
||||
"figures/Dogfood-III-bgnd-text_section.png"
|
||||
"figures/Dogfood-Intro.png"
|
||||
"figures/Dogfood-IV-jumpInDocCLass.png"
|
||||
"figures/Dogfood-V-attribute.png"
|
||||
"figures/Dogfood-VI-linkappl.png"
|
||||
"figures/isabelle-architecture.pdf"
|
||||
"figures/isabelle-architecture.svg"
|
||||
"figures/isadof.png"
|
||||
"figures/srac-as-es-application.png"
|
||||
"figures/srac-definition.png"
|
||||
"figures/Isabelle_DOF-logo.pdf"
|
||||
"figures/header_CSP_pdf.png"
|
||||
"figures/header_CSP_source.png"
|
||||
|
|
Before Width: | Height: | Size: 85 KiB |
Before Width: | Height: | Size: 43 KiB |
Before Width: | Height: | Size: 135 KiB |
Before Width: | Height: | Size: 73 KiB |
Before Width: | Height: | Size: 81 KiB |
Before Width: | Height: | Size: 37 KiB |
Before Width: | Height: | Size: 26 KiB |
|
@ -36,8 +36,6 @@
|
|||
\title{<TITLE>}
|
||||
\author{<AUTHOR>}
|
||||
|
||||
%\renewcommand{\listofSRACs}{\relax}
|
||||
%\renewcommand{\listofECs}{\relax}
|
||||
\pagestyle{headings}
|
||||
|
||||
\uppertitleback{
|
||||
|
|
|
@ -72,10 +72,6 @@ text\<open>
|
|||
@{boxed_bash [display]\<open>ë\prompt{}ë tar xf ë\href{\isadofarchiveurl}{\isadofarchiven}ë\<close>}
|
||||
This will create a directory \texttt{\isadofdirn} containing \<^isadof> distribution.
|
||||
|
||||
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
|
||||
|
|