diff -r 7f3760f39bdc -r f8845fc8f38d src/Doc/isac/jrocnik/references.bib
--- a/src/Doc/isac/jrocnik/references.bib	Mon Sep 16 12:27:20 2013 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,142 +0,0 @@
-@book{proakis2004contemporary,
-  title={Contemporary communication systems using MATLAB and Simulink},
-  author={Proakis, J.G. and Salehi, M. and Bauch, G.},
-  isbn={9780534406172},
-  lccn={31054410},
-  series={BookWare companion series},
-  url={http://books.google.at/books?id=5mXGQgAACAAJ},
-  year={2004},
-  publisher={Thomson--Brooks/Cole}
-}
-@book{oppenheim2010discrete,
-  title={Discrete-time signal processing},
-  author={Oppenheim, A.V. and Schafer, R.W.},
-  isbn={9780131988422},
-  series={Prentice-Hall signal processing series},
-  url={http://books.google.at/books?id=mYsoAQAAMAAJ},
-  year={2010},
-  publisher={Prentice Hall}
-}
-@manual{wenzel2011system,
-	title={The Isabelle System Manual},
-	author={Wenzel, M. and Berghofer, S.},
-	organization={TU Muenchen},
-	year={2011},
-	month={January}
-}
-@Book{Nipkow-Paulson-Wenzel:2002,
-  author	= {Tobias Nipkow and Lawrence C. Paulson and Markus Wenzel},
-  title		= {{Isabelle/HOL} --- A Proof Assistant for Higher-Order Logic},
-  publisher	= {Springer},
-  series	= {LNCS},
-  volume	= 2283,
-  year		= 2002}
-@Book{progr-mathematica,
-  author = 	 {Maeder, Roman E.},
-  title = 	 {Programming in Mathematica},
-  publisher = 	 {Addison-Wesley},
-  address = 	 {Reading, Mass.},
-  year = 	 {1997}
-}
-@Book{prog-maple06,
-  author = 	 {Aladjav, Victor and Bogdevicius, Marijonas},
-  title = 	 {Maple: Programming, Physical and Engineering Problems},
-  publisher = 	 {Fultus Corporation},
-  year = 	 {2006},
-  month = 	 {February 27},
-  annote = 	 {ISBN: 1596820802}
-}
-@Article{plmms10,
-  author = 	 {Florian Haftmann and Cezary Kaliszyk and Walther Neuper},
-  title = 	 {{CTP}-based programming languages~? Considerations about an experimental design},
-  journal = 	 {ACM Communications in Computer Algebra},
-  year = 	 {2010},
-  volume = 	 {44},
-  number = 	 {1/2},
-  pages = 	 {27-41} %,
-  %month = 	 {March/June},
-  %note = 	 {http://www.ist.tugraz.at/projects/isac/publ/plmms-10.pdf}
-}
-@inproceedings{casproto,
-  author    = {Cezary Kaliszyk and
-               Freek Wiedijk},
-  title     = {Certified Computer Algebra on Top of an Interactive Theorem
-               Prover},
-  booktitle = {Calculemus},
-  year      = {2007},
-  pages     = {94-105},
-  ee        = {http://dx.doi.org/10.1007/978-3-540-73086-6_8},
-  crossref  = {DBLP:conf/mkm/2007},
-  bibsource = {DBLP, http://dblp.uni-trier.de}
-}
-@InProceedings{wn:lucas-interp-12,
-  author = 	 {Neuper, Walther},
-  title = 	 {Automated Generation of User Guidance by Combining Computation and Deduction},
-  booktitle = {THedu'11: CTP-compontents for educational software},
-  year = 	 {2012},
-  editor = 	 {Quaresma, Pedro},
-  publisher = {EPTCS},
-  note = {To appear}
-}
-@Manual{Huet_all:94,
-  author = 	 {Huet, G. and Kahn, G. and  Paulin-Mohring, C.},
-  title = 	 {The Coq Proof Assistant},
-  institution =  {INRIA-Rocquencourt},
-  year = 	 {1994},
-  type = 	 {Tutorial},
-  number = 	 {Version 5.10},
-  address = 	 {CNRS-ENS Lyon},
-  status={},source={Theorema},location={-}
-}
-@TECHREPORT{Back-SD09,
-  author = {Back, Ralph-Johan},
-  title = {Structured Derivations as a Unified Proof Style for Teaching Mathematics},
-  institution = {TUCS - Turku Centre for Computer Science},
-  year = {2009},
-  type = {TUCS Technical Report},
-  number = {949},
-  address = {Turku, Finland},
-  month = {July}
-}
-@InProceedings{ActiveMath-MAIN11,
-  author = 	 {Melis, Erica and Siekmann, Jörg},
-  title = 	 {An Intelligent Tutoring System for Mathematics},
-  booktitle = {Seventh International Conference Artificial Intelligence and Soft Computing (ICAISC)},
-  pages = 	 {91-101},
-  year = 	 {2004},
-  editor = 	 {Rutkowski, L. and Siekmann, J. and Tadeusiewicz, R. and Zadeh, L.A.},
-  number = 	 {3070,},
-  series = 	 {LNAI},
-  publisher = {Springer-Verlag},
-  doi =          {doi:10.1007/978-3-540-24844-6\_12}}
-@TechReport{mat-tutor-cmu-MAIN11,
-  author = 	 {John R. Anderson},
-  title = 	 {Intelligent Tutoring and High School Mathematics},
-  institution =  {Carnegie Mellon University, Department of Psychology},
-  year = 	 {2008},
-  type = 	 {Technical Report},
-  number = 	 {20},
-  note = 	 {http://repository.cmu.edu/psychology/20}
-}
-@PhdThesis{proof-strategies-11,
-  author = 	 {Dietrich, Dominik},
-  title = 	 {Proof Planning with Compiled Strategies},
-  school = 	 {FR 6.2 Informatik, Saarland University},
-  year = 	 {2011}
-}
-@proceedings{DBLP:conf/mkm/2007,
-  editor    = {Manuel Kauers and
-               Manfred Kerber and
-               Robert Miner and
-               Wolfgang Windsteiger},
-  title     = {Towards Mechanized Mathematical Assistants, 14th Symposium,
-               Calculemus 2007, 6th International Conference, MKM 2007,
-               Hagenberg, Austria, June 27-30, 2007, Proceedings},
-  booktitle = {Calculemus/MKM},
-  publisher = {Springer},
-  series    = {Lecture Notes in Computer Science},
-  volume    = {4573},
-  year      = {2007},
-  isbn      = {978-3-540-73083-5},
-  bibsource = {DBLP, http://dblp.uni-trier.de}
-}