README.html
changeset 10079 0d78784176f4
parent 9927 7a9652294fe0
child 11066 ceab8d437b96
equal deleted inserted replaced
10078:8bb4b66cd6b5 10079:0d78784176f4
    78 
    78 
    79 
    79 
    80 <h2>User interface</h2>
    80 <h2>User interface</h2>
    81 
    81 
    82 The canonical Isabelle user interface is <a
    82 The canonical Isabelle user interface is <a
    83 href="http://www.dcs.ed.ac.uk/home/proofgen/">Proof General</a> by
    83 href="http://www.proofgeneral.org">Proof General</a> by David Aspinall
    84 David Aspinall and others.  It is a generic (X)Emacs interface for
    84 and others.  It is a generic (X)Emacs interface for proof assistants,
    85 proof assistants, including Isabelle (both for the classic and Isar
    85 including Isabelle (both for the classic and Isar version).  Proof
    86 version).  Proof General is suitable for use by pacifists and Emacs
    86 General is suitable for use by pacifists and Emacs militants
    87 militants alike. Its most prominent feature is script management,
    87 alike. Its most prominent feature is script management, providing a
    88 providing a metaphor of <em>live proof script editing</em>.  Proof
    88 metaphor of <em>live proof script editing</em>.  Proof General has
    89 General has recently gained a rather large following of both beginning
    89 recently gained a rather large following of both beginning and expert
    90 and expert users of Isabelle.
    90 users of Isabelle.
    91 
    91 
    92 <p>
    92 <p>
    93 
    93 
    94 Proof~General may be used together with the Emacs
    94 Proof~General may be used together with the Emacs
    95 <a href="http://www.fmi.uni-passau.de/~wedler/x-symbol/">
    95 <a href="http://www.fmi.uni-passau.de/~wedler/x-symbol/">