@misc(url-4ferries,
 title        = {4ferries},
 howpublished = {\url{https://fourferries.com/en/home/}},
)
@misc(url-isac-history-eptcs,
 title        = {Isac-project},
 howpublished = {\url{http://www.ist.tugraz.at/isac/History}},
)
@misc(url-mathtoys,
 title        = {Mathtoys},
 howpublished = {\url{http://mathtoys.org/}},
)
@misc(url-isac-publ,
 title        = {Publications in the \textit{ISAC}-project},
 howpublished = {\url{http://www.ist.tugraz.at/isac/Publications_and_Theses}},
)
@misc(url-movie-sub-problems,
 title        = {Slide movie on specifying sub-problems and determining a sequence},
 howpublished = {\url{http://www.ist.tugraz.at/projects/isac/publ/movie-sub-problems.pdf}},
)
@misc(url-isabelle-team,
 title        = {Team of the Isabelle project},
 howpublished = {\url{https://www21.in.tum.de/}},
)
@misc(url-isac-team,
 title        = {Team of the \textit{ISAC}-project},
 howpublished = {\url{http://www.ist.tugraz.at/isac/Credits}},
)
@inproceedings(aspinall:proof-gen,
 author       = {David Aspinall},
 year         = {2000},
 title        = {Proof General: A Generic Tool for Proof Development},
 booktitle    = {Tools and Algorithms for the Construction and Analysis of Systems},
 series       = {LNCS},
 volume       = {1785},
 organization = {TACAS},
 pages        = {38--43},
 doi          = {10.1007/3-540-46419-0_3},
)
@book(pl:baader98,
 author       = {Franz Baader and Tobias Nipkow},
 year         = {1998},
 title        = {Term Rewriting and All That},
 publisher    = {Cambridge University Press},
 address      = {Cambridge},
 doi          = {10.1017/CBO9781139172752},
)
@inbook(blanch:dis-proof-11,
 author       = {Jasmin Christian Blanchette and Lukas Bulwahn and Tobias Nipkow},
 year         = {2011},
 title        = {Automatic Proof and Disproof in Isabelle/HOL},
 pages        = {12--27},
 publisher    = {Springer Berlin Heidelberg},
 address      = {Berlin, Heidelberg},
 doi          = {10.1007/978-3-642-24364-6_2},
)
@mastersthesis(darocy:master,
 author       = {Gabriella Dar\'oczy},
 year         = {2013},
 title        = {Cognitive Aspects of Designing Dialogues in Theorem-Prover Based Mathematics Assistants; Implementation of Error-Patterns Guiding Dialogues in \textit{ISAC}},
 school       = {ME:CogSci},
 address      = {Vienna, Austria},
 note         = {{\url{http://www.ist.tugraz.at/projects/isac/publ/gdaroczy-ma.pdf}}},
)
@mastersthesis(fink:da,
 author       = {Thomas Maximilian Fink},
 year         = {2001},
 title        = {{B}enutzerschnittstelle f\"ur ein {M}athematik-{L}ernsystem im {WWW}},
 school       = {University of Technology, Institute for Softwaretechnology},
 address      = {Graz, Austria},
 note         = {\url{http://www.ist.tugraz.at/projects/isac/publ/tf-dipl.pdf}},
)
@incollection(goedel-thms,
 author       = {Kurt {G\"odel}},
 year         = {1986},
 editor       = {Feferman et al.},
 booktitle    = {Collected Works I. Publications 1929-1936},
 publisher    = {Oxford University Press},
 address      = {Oxford},
 pages        = {144--195},
 note         = {Translation from: \"Uber formal unentscheidbare S\"atze der Principia Mathematica und verwandter Systeme I, 1931},
)
@mastersthesis(MG:thesis,
 author       = {Matthias Goldgruber},
 year         = {2003},
 title        = {{Algebraische Simplifikation mittels Rewriting in \textit{ISAC}}},
 school       = {University of Technology, Institute for Softwaretechnology},
 address      = {Graz, Austria},
 note         = {\url{http://www.ist.tugraz.at/projects/isac/publ/DA-M02-main.ps.gz}},
)
@mastersthesis(RG04:thesis,
 author       = {Richard Gradischnegg},
 year         = {2004},
 title        = {Eine Java/SML--Schnittstelle f\"ur \textit{ISAC}{} auf Basis von XML},
 school       = {University of Applied Sciences, Dpt. Software Engineering},
 address      = {Hagenberg, Upper Austria},
 note         = {\url{www.ist.tugraz.at/projects/isac/publ/da-gradischnegg.ps.gz}},
)
@mastersthesis(AG:thesis,
 author       = {Andreas Griesmayer},
 year         = {2003},
 title        = {{Architecture and Knowledge-Represenation of the Web-based Math-Learning-System \textit{ISAC}}},
 school       = {University of Technology, Institute for Softwaretechnology},
 address      = {Graz, Austria},
 note         = {\url{www.ist.tugraz.at/projects/isac/publ/da-griesmayer.pdf}},
)
@manual(codegen-tutorial-17,
 author       = {Florian Haftmann},
 year         = {2017},
 title        = {Code generation from {Isabelle/HOL} theories},
 organization = {Theorem Proving Group at TUM},
 address      = {Munich},
 url          = {http://isabelle.in.tum.de/dist/Isabelle2017/doc/codegen.pdf},
 note         = {Part of the Isabelle distribution},
)
@mastersthesis(MH04:thesis,
 author       = {Mario Hochreiter},
 year         = {2004},
 title        = {Design and Implementation of a Graphical User Interface for the Math-Learning-System \textit{ISAC}},
 school       = {University of Applied Sciences, Dpt. Software Engineering},
 address      = {Hagenberg, Upper Austria},
 note         = {\url{www.ist.tugraz.at/projects/isac/publ/da-hochreiter.ps.gz}},
)
@inbook(Hupel2016,
 author       = {Lars Hupel and Viktor Kuncak},
 year         = {2016},
 title        = {Translating Scala Programs to Isabelle/HOL},
 pages        = {568--577},
 publisher    = {Springer International Publishing},
 address      = {Cham},
 doi          = {10.1007/978-3-319-40229-1_38},
)
@mastersthesis(nkarl:master,
 author       = {Natalie Karl},
 year         = {2016},
 title        = {Developing an Inclusive Approach for Representing Mathematical Formulas},
 school       = {Hagenberg University of Applied Sciences},
 address      = {Linz, Austria},
 note         = {{\url{http://www.ist.tugraz.at/projects/isac/publ/Masterthesis_NatalieKarl.pdf}}},
)
@mastersthesis(mkienl-bakk,
 author       = {Markus Kienleitner},
 year         = {2012},
 title        = {Towards ``NextStep Userguidance'' in a Mechanized Math Assistant},
 school       = {IICM, Graz University of Technology},
 note         = {{\url{http://www.ist.tugraz.at/projects/isac/publ/mkienl_bakk.pdf}}},
)
@mastersthesis(fkober-bakk,
 author       = {Franz Kober},
 year         = {2012},
 title        = {Logging of High-Level Steps in a Mechanized Math Assistant},
 school       = {IICM, Graz University of Technology},
 note         = {{\url{http://www.ist.tugraz.at/projects/isac/publ/fkober_bakk.pdf}}},
)
@inbook(Korp2009,
 author       = {Martin Korp and Christian Sternagel and Harald Zankl and Aart Middeldorp},
 year         = {2009},
 title        = {Tyrolean Termination Tool 2},
 pages        = {295--304},
 publisher    = {Springer Berlin Heidelberg},
 address      = {Berlin, Heidelberg},
 doi          = {10.1007/978-3-642-02348-4_21},
)
@phdthesis(krauss:funs,
 author       = {Alexander Krauss},
 year         = {2009},
 title        = {Automating Recursive Definitions and Termination Proofs in Higher-Order Logic},
 school       = {Technische Universit\"at M\"unchen},
)
@mastersthesis(AK04:thesis,
 author       = {Alan Krempler},
 year         = {2005},
 title        = {Architectural Design for Integrating an Interactive Dialogguide into a Mathematical Tutoring System},
 school       = {University of Technology, Institute for Softwaretechnology},
 address      = {Graz, Austria},
 note         = {{\url{http://www.ist.tugraz.at/projects/isac/publ/da-krempler.pdf}}},
)
@inproceedings(kremp.np:assess,
 author       = {Alan Krempler and Walther Neuper},
 year         = {2008},
 title        = {Formative Assessment for User Guidance in Single Stepping Systems},
 editor       = {Michael E. Aucher},
 booktitle    = {Interactive Computer Aided Learning, Proceedings of ICL08},
 address      = {Villach, Austria},
 note         = {{\url{http://www.ist.tugraz.at/projects/isac/publ/icl08.pdf}}},
)
@mastersthesis(richard:da,
 author       = {Richard Lang},
 year         = {2003},
 title        = {{Elementare Gleichungen der Mittelschulmathematik in der \textit{ISAC}Wissensbasis}},
 school       = {University of Technology, Institute of Software Technology},
 address      = {Graz, Austria},
 note         = {{\url{http://www.ist.tugraz.at/projects/isac/publ/da-rlang.ps.gz}}},
)
@mastersthesis(mlehnf:bakk-11,
 author       = {Mathias Lehnfeld},
 year         = {2011},
 title        = {Verbindung von 'Computation' und 'Deduction' im \textit{ISAC}-System},
 school       = {Institut f\"ur Computersprachen, Technische Universit\"at Wien},
 note         = {Bakkalaureate project},
)
@inbook(Lueth2013,
 author       = {Christoph L{\"u}th and Martin Ring},
 year         = {2013},
 title        = {A Web Interface for Isabelle: The Next Generation},
 pages        = {326--329},
 publisher    = {Springer Berlin Heidelberg},
 address      = {Berlin, Heidelberg},
 doi          = {10.1007/978-3-642-39320-4_22},
)
@book(progr-mathematica-2012,
 author       = {Roman E. Maeder},
 year         = {2012},
 title        = {Programming in Mathematica},
 edition      = {3rd},
 publisher    = {Addison-Wesley},
 address      = {Reading, Mass.},
)
@mastersthesis(mmahringer,
 author       = {Marco Mahringer},
 year         = {2018},
 title        = {Formula Editors for TP-based Systems. State of the Art and Prototype Implementation in \textit{ISAC}},
 school       = {University of Applied Sciences},
 address      = {Hagenberg, Austria},
 note         = {{\url{http://www.ist.tugraz.at/projects/isac/publ/mmahringer-master.pdf}}},
)
@phdthesis(wn:diss,
 author       = {Walther Neuper},
 year         = {2001},
 title        = {Reactive User-Guidance by an Autonomous Engine Doing High-School Math},
 school       = {IICM - Inst. f. Softwaretechnology},
 address      = {Technical University, A-8010 Graz},
 note         = {\url{http://www.ist.tugraz.at/projects/isac/publ/wn-diss.ps.gz}},
)
@techreport(imst-htl06,
 author       = {Walther Neuper},
 year         = {2006},
 title        = {{Angewandte Mathematik und Fachtheorie}},
 type         = {Technical Report},
 number       = {357},
 institution  = {IMST -- Innovationen Machen Schulen Top!},
 address      = {University of Klagenfurt, Institute of Instructional and School Development (IUS), 9010 Klagenfurt, Sterneckstrasse 15},
 note         = {{\relax\fontsize {9}{11}\selectfont\abovedisplayskip 8\p@ plus2\p@ minus4\p@ \abovedisplayshortskip\z@ plus\p@ \belowdisplayshortskip4\p@ plus2\p@ minus2\p@ \def\leftmargin \leftmargini\parsep 2.5\p@ plus1.5\p@ minus\p@ \topsep5\p@ plus2\p@ minus5\p@ \itemsep2.5\p@ plus1.5\p@ minus\p@ {\leftmargin\leftmargini \topsep4\p@ plus2\p@ minus2\p@ \parsep2\p@ plus\p@ minus\p@ \itemsep\parsep }\belowdisplayskip\abovedisplayskip $\tmspace+\thinmuskip{.1667em}$\newline\url {http://imst.uni-klu.ac.at/imst-wiki/index.php/Angewandte\_Mathematik\_und\_Fachtheorie}}},
)
@inproceedings(wn:lucas-interp-12,
 author       = {Walther Neuper},
 year         = {2012},
 title        = {Automated Generation of User Guidance by Combining Computation and Deduction},
 editor       = {Quaresma and Back},
 pages        = {82--101},
 doi          = {10.4204/EPTCS.79.5},
 note         = {\url{http://eptcs.web.cse.unsw.edu.au/paper.cgi?THedu11.5}},
)
@inproceedings(wneuper:gcd-coimbra,
 author       = {Walther Neuper},
 year         = {2014},
 title        = {{GCD} --- A Case Study on Lucas-Interpretation},
 booktitle    = {Joint Proceedings of the MathUI, OpenMath and ThEdu Workshops and Work in Progress track at CICM},
 address      = {Coimbra, Portugal},
 note         = {\url{http://ceur-ws.org/Vol-1186/paper-17.pdf}},
)
@inproceedings(thedu16:lucin-user-view,
 author       = {Walther Neuper},
 year         = {2016},
 title        = {Lucas-Interpretation from Users' Perspective},
 booktitle    = {Joint Proceedings of the FM4M, MathUI, and ThEdu Workshops, Doctoral Program, and Work in Progress at the Conference on Intelligent Computer Mathematics},
 address      = {Bialystok, Poland},
 pages        = {83--89},
 note         = {\url{http://cicm-conference.org/2016/ceur-ws/CICM2016-WIP.pdf}},
)
@article(wn:sys-eng-edu,
 author       = {Walther Neuper},
 year         = {2017},
 title        = {Formal Abstraction in Engineering Education --- Challenges and Technology Support},
 journal      = {Acta Didactica Napocensia},
 volume       = {10},
 number       = {1},
 doi          = {10.24193/adn.10.1.1},
 note         = {With sect.no. \url{http://www.ist.tugraz.at/projects/isac/publ/sys-explain-eng-edu.pdf}},
)
@techreport(imst-htl07,
 author       = {Walther Neuper and Christian D\"urnsteiner},
 year         = {2007},
 title        = {{Angewandte Mathematik und Fachtheorie mithilfe adaptierter Basis-Software}},
 type         = {Technical Report},
 number       = {683},
 institution  = {IMST -- Innovationen Machen Schulen Top!},
 address      = {University of Klagenfurt, Institute of Instructional and School Development (IUS), 9010 Klagenfurt, Sterneckstrasse 15},
 note         = {{\relax\fontsize {9}{11}\selectfont\abovedisplayskip 8\p@ plus2\p@ minus4\p@ \abovedisplayshortskip\z@ plus\p@ \belowdisplayshortskip4\p@ plus2\p@ minus2\p@ \def\leftmargin \leftmargini\parsep 2.5\p@ plus1.5\p@ minus\p@ \topsep5\p@ plus2\p@ minus5\p@ \itemsep2.5\p@ plus1.5\p@ minus\p@ {\leftmargin\leftmargini \topsep4\p@ plus2\p@ minus2\p@ \parsep2\p@ plus\p@ minus\p@ \itemsep\parsep }\belowdisplayskip\abovedisplayskip $\tmspace+\thinmuskip{.1667em}$\newline\url {https://www.imst.ac.at/imst-wiki/images/f/f9/683_Kurzfassung_Neuper.pdf}}},
)
@techreport(imst-hpts08,
 author       = {Walther Neuper and Johannes Reitinger},
 year         = {2008},
 title        = {{Begreifen und Mechanisieren beim Algebra Einstieg}},
 type         = {Technical Report},
 number       = {1063},
 institution  = {IMST -- Innovationen Machen Schulen Top!},
 address      = {University of Klagenfurt, Institute of Instructional and School Development (IUS), 9010 Klagenfurt, Sterneckstrasse 15},
 note         = {{\relax\fontsize {9}{11}\selectfont\abovedisplayskip 8\p@ plus2\p@ minus4\p@ \abovedisplayshortskip\z@ plus\p@ \belowdisplayshortskip4\p@ plus2\p@ minus2\p@ \def\leftmargin \leftmargini\parsep 2.5\p@ plus1.5\p@ minus\p@ \topsep5\p@ plus2\p@ minus5\p@ \itemsep2.5\p@ plus1.5\p@ minus\p@ {\leftmargin\leftmargini \topsep4\p@ plus2\p@ minus2\p@ \parsep2\p@ plus\p@ minus\p@ \itemsep\parsep }\belowdisplayskip\abovedisplayskip $\tmspace+\thinmuskip{.1667em}$\newline\url {http://imst.uni-klu.ac.at/imst-wiki/index.php/Begreifen\_und\_Mechanisieren\_beim\_Algebra-Einstieg}}},
)
@article(sys-of-sys-15,
 author       = {Claus Ballegaard Nielsen and Peter Gorm Larsen and John Fitzgerald and Jim Woodcock and Jan Peleska},
 year         = {2015},
 title        = {Systems of Systems Engineering: Basic Concepts, Model-Based Techniques, and Research Directions},
 journal      = {ACM Comput. Surv.},
 volume       = {48},
 number       = {2},
 pages        = {18:1--18:41},
 doi          = {10.1145/2794381},
)
@book(Nipkow-Paulson-Wenzel:2002,
 author       = {Tobias Nipkow and Lawrence C. Paulson and Markus Wenzel},
 year         = {2002},
 title        = {{Isabelle/HOL} --- A Proof Assistant for Higher-Order Logic},
 series       = {LNCS},
 volume       = {2283},
 publisher    = {Springer},
 doi          = {10.1007/3-540-45949-9},
)
@proceedings(seeheim,
 editor       = {G. E. Pfaff},
 year         = {1985},
 title        = {User Interface Management Systems: Proceedings of the Seeheim Workshop},
 publisher    = {Springer Verlag},
 address      = {Berlin},
)
@proceedings(EPTCS79,
 editor       = {Pedro Quaresma and Ralph-Johan Back},
 year         = {2012},
 title        = {{\rm Proceedings First Workshop on} CTP Components for Educational Software (THedu'11)},
 volume       = {79},
 publisher    = {Open Publishing Association},
)
@inproceedings(schrein:fin-mod-17,
 author       = {Wolfgang Schreiner and Alexander Brunhuemer and Christoph {F\"urst}},
 year         = {2018},
 title        = {Teaching the Formalization of Mathematical Theories and Algorithms via the Automatic Checking of Finite Models},
 editor       = {Walther Neuper and Pedro Quaresma},
 booktitle    = {ThEdu'17 Postproceedings},
 series       = {this volume of EPTCS},
 publisher    = {Open Publishing Association},
 organization = {Johannes Kepler University, Linz},
)
@article(Security-AFP,
 author       = {Christoph Sprenger and Ivano Somaini},
 year         = {2017},
 title        = {Developing Security Protocols by Refinement},
 journal      = {Archive of Formal Proofs},
 note         = {\url{http://isa-afp.org/entries/Security_Protocol_Refinement.html}, Formal proof development},
)
@techreport(isac:all,
 author       = {\textit{ISAC}{} Team},
 year         = {2002},
 title        = {\textit{ISAC}{} -- User Requirements Document, Software Requirements Document, Architectural Design Document, Software Design Document, Use Cases, Test Cases},
 type         = {Technical Report},
 institution  = {Institute for Softwaretechnology, University of Technology},
 note         = {\url{http://www.ist.tugraz.at/projects/isac/publ/isac-docu.pdf}},
)
@unpublished(isac-doc2,
 author       = {FH-Design Team},
 year         = {2017},
 title        = {\textit{ISAC}{}-Project: User Stories, User Requirements Document, Use Cases Document},
 note         = {\url{http://www.ist.tugraz.at/projects/isac/publ/isac-doc2.pdf}},
)
@inbook(Urban2010,
 author       = {Josef Urban and Jesse Alama and Piotr Rudnicki and Herman Geuvers},
 year         = {2010},
 title        = {A Wiki for Mizar: Motivation, Considerations, and Initial Prototype},
 pages        = {455--469},
 publisher    = {Springer Berlin Heidelberg},
 address      = {Berlin, Heidelberg},
 doi          = {10.1007/978-3-642-14128-7_38},
)
@incollection(mw:isar07,
 author       = {Makarius Wenzel},
 year         = {2007},
 title        = {Isabelle/{I}sar --- a generic framework for human-readable proof documents},
 editor       = {R. Matuszewski and A. Zalewska},
 booktitle    = {From Insight to Proof --- Festschrift in Honour of Andrzej Trybulec},
 series       = {Studies in Logic, Grammar, and Rhetoric},
 volume       = {10},
 publisher    = {University of Bialystok},
 pages        = {277--298},
)
@inproceedings(Wenzel-11:doc-orient,
 author       = {Makarius Wenzel},
 year         = {2011},
 title        = {Isabelle as document-oriented proof assistant},
 booktitle    = {Proceedings of the 18th Calculemus and 10th international conference on Intelligent computer mathematics},
 series       = {MKM'11},
 publisher    = {Springer-Verlag},
 address      = {Berlin, Heidelberg},
 pages        = {244--259},
 url          = {http://dl.acm.org/citation.cfm?id=2032713.2032732},
)
@inproceedings(makar-jedit-12,
 author       = {Makarius Wenzel},
 year         = {2012},
 title        = {Isabelle/{jEdit} — a Prover IDE within the {PIDE} framework},
 editor       = {J. Jeuring},
 booktitle    = {Conference on Intelligent Computer Mathematics (CICM 2012)},
 series       = {LNAI},
 volume       = {7362},
 publisher    = {Springer},
 pages        = {468--472},
 doi          = {10.1007/978-3-642-31374-5_38},
)
@inproceedings(DBLP:conf/itp/Wenzel14,
 author       = {Makarius Wenzel},
 year         = {2014},
 title        = {Asynchronous User Interaction and Tool Integration in Isabelle/PIDE},
 booktitle    = {Interactive Theorem Proving - 5th International Conference, {ITP} 2014, Held as Part of the Vienna Summer of Logic, {VSL} 2014, Vienna, Austria, July 14-17, 2014. Proceedings},
 pages        = {515--530},
 doi          = {10.1007/978-3-319-08970-6_33},
)
@manual(isa-impl-17,
 author       = {Makarius Wenzel},
 year         = {2017},
 title        = {The {I}sabelle/{I}sar Implementation},
 note         = {With contributions by Stefan Berghofer, Florian Haftmann and Larry Paulson},
)
@inproceedings(EPTCS79.9,
 author       = {Makarius Wenzel and Burkhart Wolff},
 year         = {2012},
 title        = {Isabelle/PIDE as Platform for Educational Tools},
 editor       = {Quaresma and Back},
 pages        = {143--153},
 doi          = {10.4204/EPTCS.79.9},
)
@mastersthesis(tzilling:master,
 author       = {Thomas Zillinger},
 year         = {n.y.},
 title        = {A General Web-Interface of an Assessment-Engine Instantiated for a TP-based Mathematics Assistant},
 school       = {University of Technology, IICM},
 address      = {Graz, Austria},
 note         = {{\url{http://www.ist.tugraz.at/projects/isac/publ/tzilling-master.pdf}}},
)