--- a/src/HOL/Induct/document/root.tex Fri Jan 20 21:56:34 2023 +0100
+++ b/src/HOL/Induct/document/root.tex Fri Jan 20 22:47:55 2023 +0100
@@ -25,4 +25,7 @@
\parindent 0pt\parskip 0.5ex
\input{session}
+\bibliographystyle{abbrv}
+\bibliography{root}
+
\end{document}
--- a/src/HOL/Library/document/root.bib Fri Jan 20 21:56:34 2023 +0100
+++ b/src/HOL/Library/document/root.bib Fri Jan 20 22:47:55 2023 +0100
@@ -6,16 +6,6 @@
note = {Unpublished}
}
-@InProceedings{Avigad-Donnelly,
- author = {Jeremy Avigad and Kevin Donnelly},
- title = {Formalizing {O} notation in {Isabelle/HOL}},
- booktitle = {Automated Reasoning: second international conference, IJCAR 2004},
- pages = {357--371},
- year = 2004,
- editor = {David Basin and Micha\"el Rusiowitch},
- publisher = {Springer}
-}
-
@Book{Oberschelp:1993,
author = {Arnold Oberschelp},
title = {Rekursionstheorie},
--- a/src/HOL/ROOT Fri Jan 20 21:56:34 2023 +0100
+++ b/src/HOL/ROOT Fri Jan 20 22:47:55 2023 +0100
@@ -225,7 +225,9 @@
Comb
PropLog
Com
- document_files "root.tex"
+ document_files
+ "root.bib"
+ "root.tex"
session "HOL-IMP" (timing) in IMP = "HOL-Library" +
options [document_variants = document]
@@ -658,12 +660,15 @@
Basic theory of lattices and orders.
"
theories CompleteLattice
- document_files "root.tex"
+ document_files
+ "root.bib"
+ "root.tex"
session "HOL-ex" (timing) in ex = "HOL-Number_Theory" +
description "
Miscellaneous examples and experiments for Isabelle/HOL.
"
+ options [document = false]
theories
Antiquote
Argo_Examples
@@ -743,6 +748,8 @@
theories [skip_proofs = false]
SAT_Examples
Meson_Test
+ document_files
+ "root.bib"
session "HOL-Isar_Examples" in Isar_Examples = "HOL-Computational_Algebra" +
description "
--- a/src/HOL/ex/CTL.thy Fri Jan 20 21:56:34 2023 +0100
+++ b/src/HOL/ex/CTL.thy Fri Jan 20 22:47:55 2023 +0100
@@ -9,7 +9,7 @@
begin
text \<open>
- We formalize basic concepts of Computational Tree Logic (CTL) \<^cite>\<open>"McMillan-PhDThesis" and "McMillan-LectureNotes"\<close> within the simply-typed
+ We formalize basic concepts of Computational Tree Logic (CTL) \<^cite>\<open>"McMillan-PhDThesis"\<close> within the simply-typed
set theory of HOL.
By using the common technique of ``shallow embedding'', a CTL formula is
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/ex/document/root.bib Fri Jan 20 22:47:55 2023 +0100
@@ -0,0 +1,18 @@
+@InProceedings{Avigad-Donnelly,
+ author = {Jeremy Avigad and Kevin Donnelly},
+ title = {Formalizing {O} notation in {Isabelle/HOL}},
+ booktitle = {Automated Reasoning: second international conference, IJCAR 2004},
+ pages = {357--371},
+ year = 2004,
+ editor = {David Basin and Micha\"el Rusiowitch},
+ publisher = {Springer}
+}
+
+@PhdThesis{McMillan-PhDThesis,
+ author = {Kenneth McMillan},
+ title = {Symbolic Model Checking --- An Approach to the State Explosion Problem},
+ school = {Carnegie Mellon University},
+ year = {1992},
+ month = {May},
+ url = {\url{http://mcmil.net/pubs/thesis.pdf}},
+}