src/HOL/document/root.bib
author nipkow
Sun Oct 22 09:10:10 2017 +0200 (2017-10-22 ago)
changeset 66893 ced164fe3bbd
parent 58623 2db1df2c8467
child 67299 ba52a058942f
permissions -rw-r--r--
derived axiom iffI as a lemma (thanks to Alexander Maletzky)
     1 @book{Birkhoff79,
     2   author =      {Garret Birkhoff},
     3   title =       {Lattice Theory},
     4   publisher =   {American Mathematical Society},
     5   year=1979
     6 }
     7 
     8 @Book{davenport92,
     9   author =	 {H. Davenport},
    10   title = 	 {The Higher Arithmetic},
    11   publisher = 	 {Cambridge University Press},
    12   year = 	 1992
    13 }
    14 
    15 @techreport{Gordon-TR68,
    16   author = "Mike Gordon",
    17   title = "{HOL}: {A} Machine Oriented Formulation of Higher-Order Logic",
    18   institution = "University of Cambridge, Computer Laboratory",
    19   number = 68,
    20   year = 1985
    21 }
    22 
    23 @book{card-book,
    24   title = {Introduction to {C}ardinal {A}rithmetic},
    25   author = {M. Holz and K. Steffens and E. Weitz},
    26   publisher = "Birkh{\"{a}}user",
    27   year = 1999,
    28 }
    29 
    30 @book{Nipkow-et-al:2002:tutorial,
    31   author =      {T. Nipkow and L. C. Paulson and M. Wenzel},
    32   title =       {{Isabelle/HOL} --- A Proof Assistant for Higher-Order Logic},
    33   series =      {LNCS},
    34   volume =      2283,
    35   year =        2002,
    36   publisher =   {Springer-Verlag}
    37 }
    38 
    39 @InProceedings{paulin-tlca,
    40   author	= {Christine Paulin-Mohring},
    41   title		= {Inductive Definitions in the System {Coq}: Rules and
    42 		 Properties},
    43   crossref	= {tlca93},
    44   pages		= {328-345}}
    45 
    46 @Proceedings{tlca93,
    47   title		= {Typed Lambda Calculi and Applications},
    48   booktitle	= {Typed Lambda Calculi and Applications},
    49   editor	= {M. Bezem and J.F. Groote},
    50   year		= 1993,
    51   publisher	= {Springer},
    52   series	= {LNCS 664}}