src/HOL/Lattice/document/root.bib
author wenzelm
Fri Oct 06 01:04:56 2000 +0200 (2000-10-06)
changeset 10157 6d3987f3aad9
child 68649 f849fc1cb65e
permissions -rw-r--r--
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
     1 
     2 @InProceedings{Bauer-Wenzel:2000:HB,
     3   author =       {Gertrud Bauer and Markus Wenzel},
     4   title =        {Computer-Assisted Mathematics at Work --- The {H}ahn-{B}anach Theorem in
     5       {I}sabelle/{I}sar},
     6   booktitle =    {Types for Proofs and Programs: TYPES'99},
     7   editor =       {Thierry Coquand and Peter Dybjer and Bengt Nordstr{\"o}m
     8                   and Jan Smith},
     9   series =       {LNCS},
    10   year =         2000
    11 }
    12 
    13 @Book{Davey-Priestley:1990,
    14   author        = {B. A. Davey and H. A. Priestley},
    15   title         = {Introduction to Lattices and Order},
    16   publisher     = {Cambridge University Press},
    17   year          = 1990}
    18 
    19 @InProceedings{Wenzel:1999:TPHOL,
    20   author =       {Markus Wenzel},
    21   title =        {{Isar} --- a Generic Interpretative Approach to Readable Formal Proof Documents},
    22   crossref =     {tphols99}}
    23 
    24 
    25 @Manual{Wenzel:2000:axclass,
    26   author        = {Markus Wenzel},
    27   title         = {Using Axiomatic Type Classes in Isabelle},
    28   year          = 2000,
    29   institution   = {TU Munich},
    30   note          = {\url{http://isabelle.in.tum.de/doc/axclass.pdf}}
    31 }
    32 
    33 @Manual{Wenzel:2000:isar-ref,
    34   author        = {Markus Wenzel},
    35   title         = {The {Isabelle/Isar} Reference Manual},
    36   year          = 2000,
    37   institution   = {TU Munich},
    38   note          = {\url{http://isabelle.in.tum.de/doc/isar-ref.pdf}}
    39 }
    40 
    41 @Proceedings{tphols99,
    42   title         = {Theorem Proving in Higher Order Logics: {TPHOLs} '99},
    43   booktitle     = {Theorem Proving in Higher Order Logics: {TPHOLs} '99},
    44   editor        = {Bertot, Y. and Dowek, G. and Hirschowitz, A. and
    45                   Paulin, C. and Thery, L.},
    46   series        = {LNCS},
    47   volume        = 1690,
    48   year          = 1999}