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