diff -r 1ca2f41770cc -r 79202e2eab6a ProgTutorial/document/root.bib
--- a/ProgTutorial/document/root.bib	Wed Aug 19 09:25:49 2009 +0200
+++ b/ProgTutorial/document/root.bib	Thu Aug 20 10:38:26 2009 +0200
@@ -10,36 +10,6 @@
                   Computing Science, Middlesex University}
 }
 
-@inproceedings{Krauss-IJCAR06,
-  author =	 {A.~Krauss},
-  title =	 {{P}artial {R}ecursive {F}unctions in {H}igher-{O}rder {L}ogic},
-  editor =	 {Ulrich Furbach and Natarajan Shankar},
-  booktitle =	 {Automated Reasoning, Third International Joint
-                  Conference, IJCAR 2006, Seattle, WA, USA, August
-                  17-20, 2006, Proceedings},
-  publisher =	 {Springer-Verlag},
-  series =	 {Lecture Notes in Computer Science},
-  volume =	 {4130},
-  year =	 {2006},
-  pages =	 {589-603}
-}
-
-@INPROCEEDINGS{Melham:1992:PIR,
-  AUTHOR =	 {T.~F.~Melham},
-  TITLE =	 {{A} {P}ackage for {I}nductive {R}elation {D}efinitions in
-                  {HOL}},
-  BOOKTITLE =	 {Proceedings of the 1991 International Workshop on
-                  the {HOL} Theorem Proving System and its
-                  Applications, {D}avis, {C}alifornia, {A}ugust
-                  28--30, 1991},
-  EDITOR =	 {Myla Archer and Jeffrey J. Joyce and Karl N. Levitt
-                  and Phillip J. Windley},
-  PUBLISHER =	 {IEEE Computer Society Press},
-  YEAR =	 {1992},
-  PAGES =	 {350--357},
-  ISBN =	 {0-8186-2460-4},
-}
-
 @Book{isa-tutorial,
   author	= {T.~Nipkow and L.~C.~Paulson and M.~Wenzel},
   title		= {Isabelle/HOL: A Proof Assistant for Higher-Order Logic},
@@ -54,73 +24,6 @@
   edition	= {2nd},
   publisher	= {Cambridge University Press}}
 
-@InCollection{Paulson-ind-defs,
-  author =	 {L.~C.~Paulson},
-  title =	 {A fixedpoint approach to (co)inductive and
-                  (co)datatype definitions},
-  booktitle =	 {Proof, Language, and Interaction: Essays in Honour
-                  of Robin Milner},
-  pages =	 {187--211},
-  publisher =	 {MIT Press},
-  year =	 2000,
-  editor =	 {G. Plotkin and C. Stirling and M. Tofte}
-}
-
-@inproceedings{Schirmer-LPAR04,
-  author =	 {N.~Schirmer},
-  title =	 {{A} {V}erification {E}nvironment for {S}equential {I}mperative
-                  Programs in {I}sabelle/{HOL}},
-  booktitle =	 "Logic for Programming, Artificial Intelligence, and
-                  Reasoning",
-  editor =	 "F. Baader and A. Voronkov",
-  year =	 2005,
-  publisher =	 "Springer-Verlag",
-  series =	 "Lecture Notes in Artificial Intelligence",
-  volume =	 3452,
-  pages =	 {398--414}
-}
-
-@TechReport{Schwichtenberg-MLCF,
-  author =	 {H.~Schwichtenberg},
-  title =	 {{M}inimal {L}ogic {f}or {C}omputable {F}unctionals},
-  institution =	 {Mathematisches Institut,
-                  Ludwig-Maximilians-Universit{\"a}t M{\"u}nchen},
-  year =	 2005,
-  month =	 {December},
-  note =	 {Available online at
-                  \url{http://www.mathematik.uni-muenchen.de/~minlog/minlog/mlcf.pdf}}
-}
-
-@inproceedings{Urban-Berghofer06,
-  author =	 {C.~Urban and S.~Berghofer},
-  title =	 {{A} {R}ecursion {C}ombinator for {N}ominal {D}atatypes
-                  {I}mplemented in {I}sabelle/{HOL}},
-  editor =	 {Ulrich Furbach and Natarajan Shankar},
-  booktitle =	 {Automated Reasoning, Third International Joint
-                  Conference, IJCAR 2006, Seattle, WA, USA, August
-                  17-20, 2006, Proceedings},
-  publisher =	 {Springer-Verlag},
-  series =	 {Lecture Notes in Computer Science},
-  volume =	 {4130},
-  year =	 {2006},
-  pages =	 {498-512}
-}
-
-@inproceedings{Wadler-AFP95,
-  author =	 {P.~Wadler},
-  title =	 {Monads for Functional Programming},
-  pages =	 {24-52},
-  editor =	 {Johan Jeuring and Erik Meijer},
-  booktitle =	 {Advanced Functional Programming, First International
-                  Spring School on Advanced Functional Programming
-                  Techniques, B{\aa}stad, Sweden, May 24-30, 1995,
-                  Tutorial Text},
-  publisher =	 {Springer-Verlag},
-  series =	 {Lecture Notes in Computer Science},
-  volume =	 {925},
-  year =	 {1995}
-}
-
 @manual{isa-imp,
   author	= {M.~Wenzel},
   title		= {The {Isabelle/Isar} Implementation},
@@ -145,3 +48,13 @@
   pages = 	 {465--483}
 }
 
+@Article{ Dyckhoff92,
+	title = "{Contraction-Free Sequent Calculi for Intuitionistic Logic}",
+	author = "R. Dyckhoff",
+	journal = "The Journal of Symbolic Logic",
+	volume = "57",
+	number = "3",
+	pages = "795--807",
+	year = "1992",
+	publisher = "JSTOR"
+}
\ No newline at end of file