added dummy citiation
authorhaftmann
Thu Jun 26 10:06:54 2008 +0200 (2008-06-26)
changeset 27367a75d71c73362
parent 27366 d0cda1ea705e
child 27368 9f90ac19e32b
added dummy citiation
src/HOL/Main.thy
src/HOL/document/root.bib
     1.1 --- a/src/HOL/Main.thy	Thu Jun 26 10:06:53 2008 +0200
     1.2 +++ b/src/HOL/Main.thy	Thu Jun 26 10:06:54 2008 +0200
     1.3 @@ -5,11 +5,11 @@
     1.4  header {* Main HOL *}
     1.5  
     1.6  theory Main
     1.7 -imports Map
     1.8 +imports Plain Map Presburger Recdef
     1.9  begin
    1.10  
    1.11  ML {* val HOL_proofs = ! Proofterm.proofs *}
    1.12  
    1.13 -ML {* path_add "~~/src/HOL/Library" *}
    1.14 +text {* See further \cite{Nipkow-et-al:2002:tutorial} *}
    1.15  
    1.16  end
     2.1 --- a/src/HOL/document/root.bib	Thu Jun 26 10:06:53 2008 +0200
     2.2 +++ b/src/HOL/document/root.bib	Thu Jun 26 10:06:54 2008 +0200
     2.3 @@ -1,3 +1,16 @@
     2.4  
     2.5 -@book{Birkhoff79,author={Garret Birkhoff},title={Lattice Theory},
     2.6 -publisher={American Mathematical Society},year=1979}
     2.7 \ No newline at end of file
     2.8 +@book{Birkhoff79,
     2.9 +  author =      {Garret Birkhoff},
    2.10 +  title =       {Lattice Theory},
    2.11 +  publisher =   {American Mathematical Society},
    2.12 +  year=1979
    2.13 +}
    2.14 +
    2.15 +@book{Nipkow-et-al:2002:tutorial,
    2.16 +  author =      {T. Nipkow and L. C. Paulson and M. Wenzel},
    2.17 +  title =       {{Isabelle/HOL} --- A Proof Assistant for Higher-Order Logic},
    2.18 +  series =      {LNCS},
    2.19 +  volume =      2283,
    2.20 +  year =        2002,
    2.21 +  publisher =   {Springer-Verlag}
    2.22 +}
    2.23 \ No newline at end of file