1 \chapter{Einf\"{u}hrung}
2 Europa ist bei Computer Theorem Provern (CTP) weltweit f\"uhrend, die zwei prominenten Prover sind Coq \cite{coq1999} und Isabelle \cite{Paulson:Isa94}.
3 Im Zuge der Weiterentwicklung der Informatik als Ingenieurs-Disziplin werden auch Anwendungsgebiete zunehmend mathematisiert \cite{db:dom-eng}, was wiederum CTP vermehrt auf den Plan ruft.
4 CTP sind bis dato in H\"anden eines relativ kleinen Kreises von Experten, von denen der Gro{\ss}teil wiederum im akademischen Bereich arbeitet und nur ein kleiner Teil in der Industrie. Diese Experten bevorzugen Keyboard-Shortcuts (vor Men\"us), reine Texte (ohne mathematische Sonderzeichen) und benutzen auch mit gro{\ss}em Aufwand hergestellte CTP-Entwicklungs-Umgebungen nicht, zum Beispiel die CoqIDE.
6 Nachdem CTP nun unaufhaltsam in Entwicklungs-Umgebungen von Software- Ingenieuren vorzudringen beginnen (siehe zum Beispiel \cite{aichernig:uni-iist-02,aichernig:mut-test}),% \cite{wolff10-boogie},
7 stellt sich die Herausforderung neu, Frontends f\"ur die t\"agliche Entwicklungsarbeit mit integrierten CTP zu entwerfen. Einer der Vorschl\"age, wie Theorem Prover mit Front-ends zu verbinden w\"are, findet sich in \cite{Aspinall:2007:FIP:1420412.1420429}. Isabelle geht einen anderen Weg, indem es sich aktuellen technischen Herausforderungen stellt \cite{makarius:isa-scala-jedit}: Multicore-Maschinen versprechen erh\"ohten Durchsatz, falls Teile von Beweisen parallel abgearbeitet werden k\"onnen. Isabelles Entwurf sieht vor, die Programmsprache Scala (insbesonders seine Actor-Library) als Bindeglied zwischen der Mathematik-Sprache SML und der g\"angisten Plattform f\"ur GUIs vor, der Java-Virtual-Maschine.
9 Die Bachelorarbeit l\"auft im Rahmen des ISAC-Projektes. ISACs experimenteller Mathematik-Assistant baut auf dem SML-Teil von Isabelle auf und es ist geplant, auch sein Frontend in entsprechend geplanten Schritten an die aktuelle Entwicklung von Isabelle anzuschlie{\ss}en. Der erste Schritt geht einen Umweg, um die Technologie kennen zu lernen: Nicht ISACs Rechnungen (mit aufw\"andigen Interaktionen), sondern Backs 'structured derivations' (SD) \cite{back-grundy-wright-98} sollen auf jEdit und Isabelle aufgesetzt werden. Die Bachelorarbeit liefert die Machbarkeits-Studie f\"ur diesen Schritt.