@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}

 }

 @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}

 }

 @InProceedings{gdaroczy-EP-13,

   author = 	 {Gabriella Dar\'{o}czy and Walther Neuper},

   title = 	 {Exploitation of ``Next-Step-Guidance'' in a {TP}-based Math Assistant},

   OPTpages = 	 {TODO-TODO},

   crossref =  {eduTPS-12}

 }

 @Proceedings{eduTPS-12,

   title = 	 {Theorem-Prover based Systems for Education (eduTPS)},

   year = 	 {2013},

   OPTkey = 	 {},

   OPTbooktitle = {},

   OPTeditor = 	 {},

   OPTvolume = 	 {},

   OPTnumber = 	 {},

   OPTseries = 	 {},

   OPTaddress = 	 {},

   OPTmonth = 	 {},

   OPTorganization = {},

   publisher = {The Electronic Journal of Mathematics and Technology},

   note = 	 {to appear},

   OPTannote = 	 {}

 }

 @Misc{nipkow-prog-prove,

   author = 	 {Nipkow, Tobias},

   title = 	 {Programming and Proving in {Isabelle/HOL}},

   howpublished = {contained in the Isabelle distribution},

   month = 	 {May 22},

   year = 	 {2012}

 }

 @Book{pl:hind97,

   author = 	 {J. Roger Hindley},

   title = 	 {Basic Simple Type Theory},

   publisher = 	 {Cambridge University Press},

   year = 	 1997,

   editor =	 {S. Abramsky and P. H. Aczel and others},

   number =	 42,

   series =	 {Cambridge Tracts in Theoretical Computer Science},

   address =	 {Cambridge},

   annote =	 {97bok308}

 }

 @Article{Milner-78,

   author = 	 {Milner, R.},

   title = 	 {A Theory of Type Polymorphism in Programming},

   journal = 	 {Journal of Computer and System Science (JCSS)},

   year = 	 {1978},

   number = 	 {17},

   pages = 	 {348-374}

 }

 @inproceedings{Wenzel-11:doc-orient,

  author = {Wenzel, Makarius},

  title = {Isabelle as document-oriented proof assistant},

  booktitle = {Proceedings of the 18th Calculemus and 10th international conference on Intelligent computer mathematics},

  series = {MKM'11},

  year = {2011},

  isbn = {978-3-642-22672-4},

  location = {Bertinoro, Italy},

  pages = {244--259},

  numpages = {16},

  url = {http://dl.acm.org/citation.cfm?id=2032713.2032732},

  acmid = {2032732},

  publisher = {Springer-Verlag},

  address = {Berlin, Heidelberg},

 } 

 @InProceedings{makar-jedit-12,

   author = 	 {Makarius Wenzel},

   title = 	 {Isabelle/{jEdit} — a Prover IDE within the {PIDE} framework},

   booktitle = {Conference on Intelligent Computer Mathematics (CICM 2012)},

   year = 	 {2012},

   editor = 	 { J. Jeuring and others},

   number = 	 {7362},

   series = 	 {LNAI},

   publisher = {Springer}

 }

 @InProceedings{Makarius-09:parall-proof,

   author = 	 {Wenzel, Makarius},

   title = 	 {Parallel Proof Checking in {Isabelle/Isar}},

   booktitle = {ACM SIGSAM 2009 International Workshop on Programming Languages for Mechanized Mathematics Systems (PLMMS)},

   year = 	 {2009},

   editor = 	 {Dos Reis and L. Th\'ery},

   address = 	 {Munich},

   month = 	 {August},

   publisher = {ACM Digital library}

 }