# HG changeset patch
# User wenzelm
# Date 1674251275 -3600
# Node ID d0151eb9ecb00b85200e402c51b0a1ced5ecdd65
# Parent  28ac56e59d23037dc595d1893008f2e2b20ad448
more correct and complete bibliography;

diff -r 28ac56e59d23 -r d0151eb9ecb0 src/HOL/Induct/document/root.tex
--- 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}
diff -r 28ac56e59d23 -r d0151eb9ecb0 src/HOL/Library/document/root.bib
--- 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},
diff -r 28ac56e59d23 -r d0151eb9ecb0 src/HOL/ROOT
--- 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 "
diff -r 28ac56e59d23 -r d0151eb9ecb0 src/HOL/ex/CTL.thy
--- 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
diff -r 28ac56e59d23 -r d0151eb9ecb0 src/HOL/ex/document/root.bib
--- /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}},
+}