@@ -116,8 +116,9 @@ rich font and the ample [Emacs Unicode
116
116
support] ( http://www.emacswiki.org/emacs/UnicodeEncoding ) mechanisms.
117
117
118
118
Alternatively or additionally, you can use [ Proof General's own Unicode
119
- Tokens mode] ( /components#unicodetokens ) which provides a * presentation
120
- view* on the source text by rendering sequences of characters using
119
+ Tokens mode] ( http://proofgeneral.inf.ed.ac.uk/components#unicodetokens )
120
+ which provides a * presentation view*
121
+ on the source text by rendering sequences of characters using
121
122
symbols, fonts and positioning information (see the
122
123
[ screenshots] ( /screenshots ) for examples.)
123
124
@@ -157,14 +158,15 @@ proof assistant with surprisingly little effort.
157
158
Adapting for a new proof assistant is mainly a matter of setting some
158
159
variables with regular expressions to help parse output from the prover,
159
160
and setting other variables with commands to send to the prover. See
160
- this basic [ example
161
- instance] ( http://proofgeneral.inf.ed.ac.uk/fileshow.php?file=releases%2FProofGeneral%2Fdemoisa%2Fdemoisa-easy.el ) .
161
+ this basic [ example instance] ( https://github.com/ProofGeneral/PG/blob/master/obsolete/demoisa/demoisa-easy.el ) .
162
162
To get the most from Proof General (proof by pointing, for example), it
163
163
may be necessary to put some hooks in the output routines of the proof
164
164
assistant.
165
165
166
+ {% comment %} TODO: remove
166
167
Please feel free to download Proof General to customize it for a new
167
168
system, and [ tell us] ( /feedback ) how you get on.
169
+ {% endcomment %}
168
170
169
171
For (even) more details of Proof General's features, see the manuals and
170
172
papers on the [ documentation page] ( /doc ) .
0 commit comments