diff -r 7f3760f39bdc -r f8845fc8f38d src/Doc/isac/CTP-userinterfaces.bib
--- a/src/Doc/isac/CTP-userinterfaces.bib	Mon Sep 16 12:27:20 2013 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,161 +0,0 @@
-@inproceedings{Aspinall:2007:FIP:1420412.1420429,
- author = {Aspinall, David and L\"{u}th, Christoph and Winterstein, Daniel},
- title = {A Framework for Interactive Proof},
- booktitle = {Proceedings of the 14th symposium on Towards Mechanized Mathematical Assistants: 6th International Conference},
- series = {Calculemus '07 / MKM '07},
- year = {2007},
- isbn = {978-3-540-73083-5},
- location = {Hagenberg, Austria},
- pages = {161--175},
- numpages = {15},
- url = {http://dx.doi.org/10.1007/978-3-540-73086-6_15},
- doi = {http://dx.doi.org/10.1007/978-3-540-73086-6_15},
- acmid = {1420429},
- publisher = {Springer-Verlag},
- address = {Berlin, Heidelberg},
-}
-
-@Book{armstrong:erlang96,
-  author = 	 {Armstrong, Joe and others},
-  title = 	 {Concurrent Programming in Erlang},
-  publisher = {Prentice Hall},
-  year = 	 {1996}
-}
-
-@TechReport{odersky:scala06,
-  author = 	 {Odersky, Martin and others},
-  title = 	 {An Overview of the Scala Programming Language},
-  institution =  {\'Ecole Polytechnique F\'ed\'erale de Lausanne (EPFL)},
-  year = 	 {2006},
-  type = 	 {Technical Report LAMP-REPORT-2006-001},
-  address = 	 {1015 Lausanne, Switzerland},
-  note = 	 {Second Edition},
-  annote = 	 {http://www.scala-lang.org/sites/default/files/linuxsoft_archives/docu/files/ScalaOverview.pdf}
-}
-
-@article{Haller:2009:SAU:1496391.1496422,
- author = {Haller, Philipp and Odersky, Martin},
- title = {Scala Actors: Unifying thread-based and event-based programming},
- journal = {Theor. Comput. Sci.},
- volume = {410},
- issue = {2-3},
- month = {February},
- year = {2009},
- issn = {0304-3975},
- pages = {202--220},
- numpages = {19},
- url = {http://portal.acm.org/citation.cfm?id=1496391.1496422},
- doi = {10.1016/j.tcs.2008.09.019},
- acmid = {1496422},
- publisher = {Elsevier Science Publishers Ltd.},
- address = {Essex, UK},
- keywords = {Actors, Concurrent programming, Events, Threads},
-} 
-
-@InProceedings{scala:jmlc06,
-  author =       {Philipp Haller and Martin Odersky},
-  title =        {Event-Based Programming without Inversion of Control},
-  booktitle =    {Proc. Joint Modular Languages Conference},
-  year =         2006,
-  series =       {Springer LNCS}
-}
-
-
-@InProceedings{makarius:isa-scala-jedit,
-  author = 	 {Makarius Wenzel},
-  title = 	 {Asyncronous Proof Processing with {Isabelle/Scala} and {Isabelle/jEdit}},
-  booktitle = {User Interfaces for Theorem Provers (UITP 2010)},
-  year = 	 {2010},
-  editor = 	 {C. Sacerdoti Coen and D. Aspinall},
-  address = 	 {Edinburgh, Scotland},
-  month = 	 {July},
-  organization = {FLOC 2010 Satellite Workshop},
-  note = 	 {http://www4.in.tum.de/~wenzelm/papers/async-isabelle-scala.pdf}
-}
-
-@Book{db:dom-eng,
-  author = 	 {Bj{\o}rner, Dines},
-  title = 	 {Domain Engineering. Technology Management, Research and Engineering},
-  publisher = 	 {JAIST Press},
-  year = 	 {2009},
-  month = 	 {Feb},
-  series = 	 {COE Research Monograph Series},
-  volume = 	 {4},
-  address = 	 {Nomi, Japan}
-}
-
-@inproceedings{Haftmann-Nipkow:2010:code,
-  author =      {Florian Haftmann and Tobias Nipkow},
-  title =       {Code Generation via Higher-Order Rewrite Systems},
-  booktitle =   {Functional and Logic Programming, 10th International
-Symposium: {FLOPS} 2010},
-  year =        {2010},
-  publisher =   {Springer},
-  series =      {Lecture Notes in Computer Science},
-  volume =      {6009}
-}
-
-@Manual{coq1999,
-  title = 	 {The Coq Proof Assistant},
-  author = 	 {Barras, B. and others},
-  organization = {INRIA-Rocquencourt - CNRS-ENS Lyon},
-  month = 	 {July},
-  year = 	 {1999},
-  pnote={},status={cited},source={mkm01.caprotti},location={}  
-}
-
-@Book{meta-ML,
-  author = 	 {Gordon,M. and Milner,R.  and Wadsworth,C. P.},
-  title = 	 {Edinburgh LCF: A Mechanised Logic of Computation},
-  publisher = 	 { Springer-Verlag},
-  year = 	 {1979},
-  volume = 	 {78},
-  series = 	 {Lecture Notes in Computer Science}
-}
- 
-@book{Paulson:Isa94,
-        title={Isabelle: a generic theorem prover}, 
-        author={Paulson, Lawrence C. }, publisher={Springer-Verlag},year={1994}, 
-	volume={828},series={Lecture Notes in Computer Science},address={},edition={},month={}, 
-	note={With contributions by Topias Nipkow},
-        status={},source={},location={-} 
-        }  
-
-@Book{pl:milner97,
-  author = 	 {Robin Milner and Mads Tofte and Robert Harper and David MacQueen},
-  title = 	 {The Definition of Standard ML (Revised)},
-  publisher = 	 {The MIT Press},
-  year = 	 1997,
-  address =	 {Cambridge, London},
-  annote =	 {97bok375}
-}
-
-@Article{back-grundy-wright-98,
-  author = 	 {Back, Ralph and Grundy, Jim and von Wright, Joakim},
-  title = 	 {Structured Calculational Proof},
-  journal = 	 {Formal Aspects of Computing},
-  year = 	 {1998},
-  number = 	 {9},
-  pages = 	 {469-483}
-}
-
-@Manual{isar-impl,
-  title = 	 {The {Isabelle/Isar} Implementation},
-  author = 	 {Makarius Wenzel},
-  month = 	 {April 19},
-  year = 	 {2009},
-  note = 	 {With contributions by Florian Haftmann and Larry Paulson}
-}
-
-@InProceedings{wenzel:isar,
-  author = 	 {Wenzel, Markus},
-  title = 	 {Isar - a Generic Interpretative Approach to Readable Formal Proof Documents},
-  booktitle = 	 {Theorem Proving in Higher Order Logics},
-  year = 	 {1999},
-  editor = 	 {G. Dowek, A. Hirschowitz, C. Paulin, L. Thery},
-  series = 	 {LNCS 1690},
-  organization = {12th International Conference TPHOLs'99},
-  publisher = {Springer}
-}
-
-