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

Update Isabelle + AFP URLs

This commit is contained in:
Makarius Wenzel 2022-12-01 11:55:51 +01:00
parent c29ec9641a
commit a6ab1e101e
5 changed files with 8 additions and 8 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

4
README.md
View File

@ -10,9 +10,9 @@ online.](https://artifacts.logicalhacking.com/releases/Isabelle_DOF/Isabelle_DOF
Isabelle/DOF has three major prerequisites:
* **Isabelle:** Isabelle/DOF requires [Isabelle
2022](http://isabelle.in.tum.de/website-Isabelle2022/). Please download the
2022](https://isabelle.in.tum.de/website-Isabelle2022/). Please download the
Isabelle 2022 distribution for your operating system from the [Isabelle
website](http://isabelle.in.tum.de/website-Isabelle2022/).
website](https://isabelle.in.tum.de/website-Isabelle2022/).
* **AFP:** Isabelle/DOF requires several entries from the [Archive of Formal Proofs
(AFP)](https://www.isa-afp.org/). Please install the AFP following the
instructions given at <https://www.isa-afp.org/using.html>.

4
examples/scholarly_paper/2020-iFM-CSP/document/root.bib
View File

@ -6870,7 +6870,7 @@ isbn="978-3-540-48509-4"
title = {{Isabelle's} Logic: {HOL}},
author = {Tobias Nipkow and Lawrence C. Paulson and Markus Wenzel},
year = 2009,
misc = {\url{http://isabelle.in.tum.de/library/HOL/}}
misc = {\url{https://isabelle.in.tum.de/library/HOL/}}
}
@InProceedings{ garson.ea:security:2008,
@ -11000,7 +11000,7 @@ isbn="978-1-4471-3182-3"
journal = {Archive of Formal Proofs},
month = apr,
year = 2019,
note = {\url{http://isa-afp.org/entries/HOL-CSP.html}},
note = {\url{https://isa-afp.org/entries/HOL-CSP.html}},
ISSN = {2150-914x},
}

4
examples/technical_report/Isabelle_DOF-Manual/document/root.bib
View File

@ -451,7 +451,7 @@
journal = {Archive of Formal Proofs},
month = may,
year = 2010,
note = {\url{http://isa-afp.org/entries/Regular-Sets.html}, Formal
note = {\url{https://isa-afp.org/entries/Regular-Sets.html}, Formal
proof development},
issn = {2150-914x}
}
@ -462,7 +462,7 @@
journal = {Archive of Formal Proofs},
month = mar,
year = 2004,
note = {\url{http://isa-afp.org/entries/Functional-Automata.html},
note = {\url{https://isa-afp.org/entries/Functional-Automata.html},
Formal proof development},
issn = {2150-914x}
}

2
examples/technical_report/TR_my_commented_isabelle/TR_MyCommentedIsabelle.thy
View File

@ -62,7 +62,7 @@ text\<open> \<^vs>\<open>-0.5cm\<close>
Isabelle and Isabelle/HOL, a complementary text to the unfortunately somewhat outdated
"The Isabelle Cookbook" in \<^url>\<open>https://nms.kcl.ac.uk/christian.urban/Cookbook/\<close>.
The present text is also complementary to the current version of
\<^url>\<open>https://isabelle.in.tum.de/dist/Isabelle2021/doc/isar-ref.pdf\<close>
\<^url>\<open>https://isabelle.in.tum.de/doc/isar-ref.pdf\<close>
"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.

2
src/ontologies/Conceptual/Conceptual.thy
View File

@ -28,7 +28,7 @@ doc_class A =
subsection\<open>Excursion: On the semantic consequences of this definition: \<close>
text\<open>This class definition leads an implicit Isabelle/HOL \<^theory_text>\<open>record\<close> definition
(cf. \<^url>\<open>https://isabelle.in.tum.de/dist/Isabelle2021/doc/isar-ref.pdf\<close>, chapter 11.6.).
(cf. \<^url>\<open>https://isabelle.in.tum.de/doc/isar-ref.pdf\<close>, chapter 11.6.).
Consequently, \<^theory_text>\<open>doc_class\<close>'es inherit the entire theory-infrastructure from Isabelle records:
\<^enum> there is a HOL-type \<^typ>\<open>A\<close> and its extensible version \<^typ>\<open>'a A_scheme\<close>
\<^enum> there are HOL-terms representing \<^emph>\<open>doc_class instances\<close> with the high-level syntax: