src/HOL/Isar_examples/document/root.bib
author oheimb
Wed Jan 31 10:15:55 2001 +0100 (2001-01-31)
changeset 11008 f7333f055ef6
parent 10148 739327964a5c
child 14378 69c4d5997669
permissions -rw-r--r--
improved theory reference in comment
     1 
     2 @string{CUCL="Comp. Lab., Univ. Camb."}
     3 @string{CUP="Cambridge University Press"}
     4 @string{Springer="Springer-Verlag"}
     5 @string{TUM="TU Munich"}
     6 
     7 @Book{Concrete-Math,
     8   author = 	 {R. L. Graham and D. E. Knuth and O. Patashnik},
     9   title = 	 {Concrete Mathematics},
    10   publisher = 	 {Addison-Wesley},
    11   year = 	 1989
    12 }
    13 
    14 @InProceedings{Naraschewski-Wenzel:1998:HOOL,
    15   author	= {Wolfgang Naraschewski and Markus Wenzel},
    16   title		= {Object-Oriented Verification based on Record Subtyping in
    17                   {H}igher-{O}rder {L}ogic},
    18   crossref      = {tphols98}}
    19 
    20 @Article{Nipkow:1998:Winskel,
    21   author = 	 {Tobias Nipkow},
    22   title = 	 {Winskel is (almost) Right: Towards a Mechanized Semantics Textbook},
    23   journal = 	 {Formal Aspects of Computing},
    24   year = 	 1998,
    25   volume =	 10,
    26   pages =	 {171--186}
    27 }
    28 
    29 @InProceedings{Wenzel:1999:TPHOL,
    30   author = 	 {Markus Wenzel},
    31   title = 	 {{Isar} --- a Generic Interpretative Approach to Readable Formal Proof Documents},
    32   crossref =     {tphols99}}
    33 
    34 @Book{Winskel:1993,
    35   author = 	 {G. Winskel},
    36   title = 	 {The Formal Semantics of Programming Languages},
    37   publisher = 	 {MIT Press},
    38   year = 	 1993
    39 }
    40 
    41 @Book{davey-priestley,
    42   author	= {B. A. Davey and H. A. Priestley},
    43   title		= {Introduction to Lattices and Order},
    44   publisher	= CUP,
    45   year		= 1990}
    46 
    47 @manual{isabelle-HOL,
    48   author	= {Tobias Nipkow and Lawrence C. Paulson and Markus Wenzel},
    49   title		= {{Isabelle}'s Logics: {HOL}},
    50   institution	= {Institut f\"ur Informatik, Technische Universi\"at
    51                   M\"unchen and Computer Laboratory, University of Cambridge}}
    52 
    53 @manual{isabelle-intro,
    54   author	= {Lawrence C. Paulson},
    55   title		= {Introduction to {Isabelle}},
    56   institution	= CUCL}
    57 
    58 @manual{isabelle-isar-ref,
    59   author	= {Markus Wenzel},
    60   title		= {The {Isabelle/Isar} Reference Manual},
    61   institution	= TUM}
    62 
    63 @manual{isabelle-ref,
    64   author	= {Lawrence C. Paulson},
    65   title		= {The {Isabelle} Reference Manual},
    66   institution	= CUCL}
    67 
    68 @TechReport{paulson-mutilated-board,
    69   author = 	 {Lawrence C. Paulson},
    70   title = 	 {A Simple Formalization and Proof for the Mutilated Chess Board},
    71   institution =  CUCL,
    72   year = 	 1996,
    73   number =	 394,
    74   note = {\url{http://www.ftp.cl.cam.ac.uk/ftp/papers/reports/}}
    75 }
    76 
    77 @Proceedings{tphols98,
    78   title		= {Theorem Proving in Higher Order Logics: {TPHOLs} '98},
    79   booktitle	= {Theorem Proving in Higher Order Logics: {TPHOLs} '98},
    80   editor	= {Jim Grundy and Malcom Newey},
    81   series	= {LNCS},
    82   volume        = 1479,
    83   year		= 1998}
    84 
    85 @Proceedings{tphols99,
    86   title		= {Theorem Proving in Higher Order Logics: {TPHOLs} '99},
    87   booktitle	= {Theorem Proving in Higher Order Logics: {TPHOLs} '99},
    88   editor	= {Bertot, Y. and Dowek, G. and Hirschowitz, A. and
    89                   Paulin, C. and Thery, L.},
    90   series	= {LNCS 1690},
    91   year		= 1999}