wneuper/isa: src/HOL/ex/document/root.bib@2be514a36aec

     2 @TechReport{Gordon:1985:HOL,

     3   author =       {M. J. C. Gordon},

     4   title =        {{HOL}: A machine oriented formulation of higher order logic},

     5   institution =  {University of Cambridge Computer Laboratory},

     6   year =         1985,

     7   number =       68

8 }

    10 @InProceedings{Kamm-et-al:1999,

    11   author =       {Florian Kamm{\"u}ller and Markus Wenzel and

    12                   Lawrence C. Paulson},

    13   title =        {Locales: A Sectioning Concept for {Isabelle}},

    14   booktitle     = {Theorem Proving in Higher Order Logics: {TPHOLs} '99},

    15   editor        = {Bertot, Y. and Dowek, G. and Hirschowitz, A. and

    16                   Paulin, C. and Thery, L.},

    17   series        = {LNCS},

    18   volume        = 1690,

    19   year          = 1999}

    21 @InProceedings{Naraschewski-Wenzel:1998,

    22   author        = {Wolfgang Naraschewski and Markus Wenzel},

    23   title         = {Object-Oriented Verification based on Record Subtyping in

    24                   {H}igher-{O}rder {L}ogic},

    25   booktitle     = {Theorem Proving in Higher Order Logics: {TPHOLs} '98},

    26   editor        = {Jim Grundy and Malcom Newey},

    27   series        = {LNCS},

    28   volume        = 1479,

    29   year          = 1998}

    31 @Manual{Nipkow-et-al:2001:HOL,

    32   author        = {Tobias Nipkow and Lawrence C. Paulson and Markus Wenzel},

    33   title         = {{Isabelle}'s Logics: {HOL}},

    34   institution   = {Institut f{\"u}r Informatik, Technische Universi{\"a}t

    35                   M{\"u}nchen and Computer Laboratory, University of Cambridge},

    36   year          = 2001,

    37   note          = {Part of the Isabelle distribution,

    38                    \url{http://isabelle.in.tum.de/doc/logics-HOL.pdf}}

    39 }

    41 @Article{Paulson:1989,

    42   author =       {L. C. Paulson},

    43   title =        {The foundation of a generic Theorem Prover},

    44   journal =      {Journal of Automated Reasoning},

    45   year =         1989,

    46   volume =       5,

    47   number =       3,

    48   pages =        {363--397}

    49 }

    51 @InProceedings{Wenzel:1999,

    52   author =       {Markus Wenzel},

    53   title =        {{Isar} --- a Generic Interpretative Approach to Readable Formal Proof Documents},

    54   booktitle     = {Theorem Proving in Higher Order Logics: {TPHOLs} '99},

    55   editor        = {Bertot, Y. and Dowek, G. and Hirschowitz, A. and

    56                   Paulin, C. and Thery, L.},

    57   series        = {LNCS},

    58   volume        = 1690,

    59   year          = 1999}

    61 @Unpublished{Wenzel:2001:Isar-examples,

    62   author =       {Markus Wenzel},

    63   title =        {Miscellaneous {I}sabelle/{I}sar examples for

    64                   Higher-Order Logic},

    65   year =         2001,

    66   note =         {Part of the Isabelle distribution,

    67                   \url{http://isabelle.in.tum.de/library/HOL/Isar_examples/document.pdf}}

    68 }

    69 @PhdThesis{Wenzel:2001:Thesis,

    70   author = 	 {Markus Wenzel},

    71   title = 	 {Isabelle/Isar --- a versatile environment for human-readable

    72                   formal proof documents},

    73   school = 	 {Institut f{\"u}r Informatik, Technische Universit{\"a}t M{\"u}nchen},

    74   year = 	 2001,

    75   month =	 {September},

    76   note =	 {Submitted}

    77 }

    79 @Manual{Wenzel:2001:isar-ref,

    80   author        = {Markus Wenzel},

    81   title         = {The {Isabelle/Isar} Reference Manual},

    82   year          = 2001,

    83   institution   = {TU M{\"u}nchen},

    84   note          = {Part of the Isabelle distribution,

    85                    \url{http://isabelle.in.tum.de/doc/isar-ref.pdf}}

    86 }

author	wenzelm
	Tue, 19 Feb 2002 23:49:26 +0100
changeset 12900	2be514a36aec
parent 12508	698394a2a47f
child 13446	f0fdd0499dad
permissions	-rw-r--r--