--- a/src/HOL/Main.thy Thu Jun 26 10:06:53 2008 +0200
+++ b/src/HOL/Main.thy Thu Jun 26 10:06:54 2008 +0200
@@ -5,11 +5,11 @@
header {* Main HOL *}
theory Main
-imports Map
+imports Plain Map Presburger Recdef
begin
ML {* val HOL_proofs = ! Proofterm.proofs *}
-ML {* path_add "~~/src/HOL/Library" *}
+text {* See further \cite{Nipkow-et-al:2002:tutorial} *}
end
--- a/src/HOL/document/root.bib Thu Jun 26 10:06:53 2008 +0200
+++ b/src/HOL/document/root.bib Thu Jun 26 10:06:54 2008 +0200
@@ -1,3 +1,16 @@
-@book{Birkhoff79,author={Garret Birkhoff},title={Lattice Theory},
-publisher={American Mathematical Society},year=1979}
\ No newline at end of file
+@book{Birkhoff79,
+ author = {Garret Birkhoff},
+ title = {Lattice Theory},
+ publisher = {American Mathematical Society},
+ year=1979
+}
+
+@book{Nipkow-et-al:2002:tutorial,
+ author = {T. Nipkow and L. C. Paulson and M. Wenzel},
+ title = {{Isabelle/HOL} --- A Proof Assistant for Higher-Order Logic},
+ series = {LNCS},
+ volume = 2283,
+ year = 2002,
+ publisher = {Springer-Verlag}
+}
\ No newline at end of file