src/HOL/ex/document/root.bib
changeset 12101 a79681a01f41
child 12360 9c156045c8f2
equal deleted inserted replaced
12100:bb10ac677955 12101:a79681a01f41
       
     1 
       
     2 @InProceedings{Kamm-et-al:1999,
       
     3   author =       {Florian Kamm{\"u}ller and Markus Wenzel and
       
     4                   Lawrence C. Paulson},
       
     5   title =        {Locales: A Sectioning Concept for {Isabelle}},
       
     6   booktitle     = {Theorem Proving in Higher Order Logics: {TPHOLs} '99},
       
     7   editor        = {Bertot, Y. and Dowek, G. and Hirschowitz, A. and
       
     8                   Paulin, C. and Thery, L.},
       
     9   series        = {LNCS},
       
    10   volume        = 1690,
       
    11   year          = 1999}
       
    12 
       
    13 @InProceedings{Naraschewski-Wenzel:1998,
       
    14   author        = {Wolfgang Naraschewski and Markus Wenzel},
       
    15   title         = {Object-Oriented Verification based on Record Subtyping in
       
    16                   {H}igher-{O}rder {L}ogic},
       
    17   booktitle     = {Theorem Proving in Higher Order Logics: {TPHOLs} '98},
       
    18   editor        = {Jim Grundy and Malcom Newey},
       
    19   series        = {LNCS},
       
    20   volume        = 1479,
       
    21   year          = 1998}
       
    22 
       
    23 @Manual{Nipkow-et-al:2001:HOL,
       
    24   author        = {Tobias Nipkow and Lawrence C. Paulson and Markus Wenzel},
       
    25   title         = {{Isabelle}'s Logics: {HOL}},
       
    26   institution   = {Institut f{\"u}r Informatik, Technische Universi{\"a}t
       
    27                   M{\"u}nchen and Computer Laboratory, University of Cambridge},
       
    28   year          = 2001,
       
    29   note          = {Part of the Isabelle distribution,
       
    30                    \url{http://isabelle.in.tum.de/doc/logics-HOL.pdf}}
       
    31 }
       
    32 
       
    33 @InProceedings{Wenzel:1999,
       
    34   author =       {Markus Wenzel},
       
    35   title =        {{Isar} --- a Generic Interpretative Approach to Readable Formal Proof Documents},
       
    36   booktitle     = {Theorem Proving in Higher Order Logics: {TPHOLs} '99},
       
    37   editor        = {Bertot, Y. and Dowek, G. and Hirschowitz, A. and
       
    38                   Paulin, C. and Thery, L.},
       
    39   series        = {LNCS},
       
    40   volume        = 1690,
       
    41   year          = 1999}
       
    42 
       
    43 @PhdThesis{Wenzel:2001:Thesis,
       
    44   author = 	 {Markus Wenzel},
       
    45   title = 	 {Isabelle/Isar --- a versatile environment for human-readable
       
    46                   formal proof documents},
       
    47   school = 	 {Institut f{\"u}r Informatik, Technische Universit{\"a}t M{\"u}nchen},
       
    48   year = 	 2001,
       
    49   month =	 {September},
       
    50   note =	 {Submitted}
       
    51 }
       
    52 
       
    53 @Manual{Wenzel:2001:isar-ref,
       
    54   author        = {Markus Wenzel},
       
    55   title         = {The {Isabelle/Isar} Reference Manual},
       
    56   year          = 2001,
       
    57   institution   = {TU M{\"u}nchen},
       
    58   note          = {Part of the Isabelle distribution,
       
    59                    \url{http://isabelle.in.tum.de/doc/isar-ref.pdf}}
       
    60 }