Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/Doc/IsarRef/Preface.thy
changeset 51058 98c48d023136
parent 50109 c13dc0b1841c 
--- a/src/Doc/IsarRef/Preface.thy	Sat Jan 26 16:10:50 2013 +0100
+++ b/src/Doc/IsarRef/Preface.thy	Sat Jan 26 16:30:47 2013 +0100
@@ -17,12 +17,16 @@
   theory and proof development.  Compared to raw ML, the Isabelle/Isar
   top-level provides a more robust and comfortable development
   platform, with proper support for theory development graphs, managed
-  transactions with unlimited undo etc.  The Isabelle/Isar version of
-  the \emph{Proof~General} user interface
-  \cite{proofgeneral,Aspinall:TACAS:2000} provides a decent front-end
-  for interactive theory and proof development in this advanced
-  theorem proving environment, even though it is somewhat biased
-  towards old-style proof scripts.
+  transactions with unlimited undo etc.
+
+  In its pioneering times, the Isabelle/Isar version of the
+  \emph{Proof~General} user interface
+  \cite{proofgeneral,Aspinall:TACAS:2000} has contributed to the
+  success of for interactive theory and proof development in this
+  advanced theorem proving environment, even though it was somewhat
+  biased towards old-style proof scripts.  The more recent
+  Isabelle/jEdit Prover IDE \cite{Wenzel:2012} emphasizes the
+  document-oriented approach of Isabelle/Isar again more explicitly.
 
   \medskip Apart from the technical advances over bare-bones ML
   programming, the main purpose of the Isar language is to provide a
isabelle