src/HOL/Isar_examples/document/root.bib
author wenzelm
Thu, 28 Oct 1999 19:57:34 +0200
changeset 7968 964b65b4e433
parent 7816 2840e8857523
child 7977 67bfcd3a433c
permissions -rw-r--r--
improved presentation;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
7816
wenzelm
parents:
diff changeset
     1
wenzelm
parents:
diff changeset
     2
@string{CUCL="Comp. Lab., Univ. Camb."}
wenzelm
parents:
diff changeset
     3
@string{CUP="Cambridge University Press"}
wenzelm
parents:
diff changeset
     4
@string{Springer="Springer-Verlag"}
wenzelm
parents:
diff changeset
     5
@string{TUM="TU Munich"}
wenzelm
parents:
diff changeset
     6
wenzelm
parents:
diff changeset
     7
7968
964b65b4e433 improved presentation;
wenzelm
parents: 7816
diff changeset
     8
@InProceedings{Wenzel:1999:TPHOL,
964b65b4e433 improved presentation;
wenzelm
parents: 7816
diff changeset
     9
  author = 	 {Markus Wenzel},
964b65b4e433 improved presentation;
wenzelm
parents: 7816
diff changeset
    10
  title = 	 {{Isar} --- a Generic Interpretative Approach to Readable Formal Proof Documents},
964b65b4e433 improved presentation;
wenzelm
parents: 7816
diff changeset
    11
  crossref =     {tphols99}}
964b65b4e433 improved presentation;
wenzelm
parents: 7816
diff changeset
    12
7816
wenzelm
parents:
diff changeset
    13
@Book{davey-priestley,
wenzelm
parents:
diff changeset
    14
  author	= {B. A. Davey and H. A. Priestley},
wenzelm
parents:
diff changeset
    15
  title		= {Introduction to Lattices and Order},
wenzelm
parents:
diff changeset
    16
  publisher	= CUP,
wenzelm
parents:
diff changeset
    17
  year		= 1990}
wenzelm
parents:
diff changeset
    18
wenzelm
parents:
diff changeset
    19
@manual{isabelle-HOL,
wenzelm
parents:
diff changeset
    20
  author	= {Tobias Nipkow and Lawrence C. Paulson and Markus Wenzel},
wenzelm
parents:
diff changeset
    21
  title		= {{Isabelle}'s Logics: {HOL}},
wenzelm
parents:
diff changeset
    22
  institution	= {Institut f\"ur Informatik, Technische Universi\"at
wenzelm
parents:
diff changeset
    23
                  M\"unchen and Computer Laboratory, University of Cambridge}}
wenzelm
parents:
diff changeset
    24
wenzelm
parents:
diff changeset
    25
@manual{isabelle-intro,
wenzelm
parents:
diff changeset
    26
  author	= {Lawrence C. Paulson},
wenzelm
parents:
diff changeset
    27
  title		= {Introduction to {Isabelle}},
wenzelm
parents:
diff changeset
    28
  institution	= CUCL}
wenzelm
parents:
diff changeset
    29
wenzelm
parents:
diff changeset
    30
@manual{isabelle-isar-ref,
wenzelm
parents:
diff changeset
    31
  author	= {Markus Wenzel},
7968
964b65b4e433 improved presentation;
wenzelm
parents: 7816
diff changeset
    32
  title		= {The {Isabelle/Isar} Reference Manual},
7816
wenzelm
parents:
diff changeset
    33
  institution	= TUM}
wenzelm
parents:
diff changeset
    34
7968
964b65b4e433 improved presentation;
wenzelm
parents: 7816
diff changeset
    35
@manual{isabelle-ref,
964b65b4e433 improved presentation;
wenzelm
parents: 7816
diff changeset
    36
  author	= {Lawrence C. Paulson},
964b65b4e433 improved presentation;
wenzelm
parents: 7816
diff changeset
    37
  title		= {The {Isabelle} Reference Manual},
964b65b4e433 improved presentation;
wenzelm
parents: 7816
diff changeset
    38
  institution	= CUCL}
964b65b4e433 improved presentation;
wenzelm
parents: 7816
diff changeset
    39
964b65b4e433 improved presentation;
wenzelm
parents: 7816
diff changeset
    40
@TechReport{paulson-mutilated-board,
964b65b4e433 improved presentation;
wenzelm
parents: 7816
diff changeset
    41
  author = 	 {Lawrence C. Paulson},
964b65b4e433 improved presentation;
wenzelm
parents: 7816
diff changeset
    42
  title = 	 {A Simple Formalization and Proof for the Mutilated Chess Board},
964b65b4e433 improved presentation;
wenzelm
parents: 7816
diff changeset
    43
  institution =  CUCL,
964b65b4e433 improved presentation;
wenzelm
parents: 7816
diff changeset
    44
  year = 	 1996,
964b65b4e433 improved presentation;
wenzelm
parents: 7816
diff changeset
    45
  number =	 394,
964b65b4e433 improved presentation;
wenzelm
parents: 7816
diff changeset
    46
  note = {\url{http://www.ftp.cl.cam.ac.uk/ftp/papers/reports/TR394-lcp-mutilated-chess-board.pdf}}
964b65b4e433 improved presentation;
wenzelm
parents: 7816
diff changeset
    47
}
7816
wenzelm
parents:
diff changeset
    48
wenzelm
parents:
diff changeset
    49
@Proceedings{tphols99,
wenzelm
parents:
diff changeset
    50
  title		= {Theorem Proving in Higher Order Logics: {TPHOLs} '99},
wenzelm
parents:
diff changeset
    51
  booktitle	= {Theorem Proving in Higher Order Logics: {TPHOLs} '99},
wenzelm
parents:
diff changeset
    52
  editor	= {Bertot, Y. and Dowek, G. and Hirschowitz, A. and
wenzelm
parents:
diff changeset
    53
                  Paulin, C. and Thery, L.},
wenzelm
parents:
diff changeset
    54
  series	= {LNCS 1690},
wenzelm
parents:
diff changeset
    55
  year		= 1999}