| Age | Commit message (Collapse) | Author |
|---|
|
improved regexps and font-lock;
|
|
|
|
do not append '/' to PROOFGENERAL_HOME;
|
|
improved isar-find-and-forget;
|
|
|
|
|
|
the function coq-guess-command-line in the coq part. Every prover
should have the functon *-guess-command-line that uses, for example,
the output of "make -n" to guess the correct command line options of
the prover.
Patrick
|
|
|
|
|
|
based on the lego instantiation.
|
|
|
|
|
|
|
|
|
|
|
|
end with a slash. Moreover, the closure proof-home-directory-fn is
added so that this value is not computed at compilation time.
|
|
|
|
|
|
|
|
tuned "next";
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
o added a suggestion by hht
o documentation now at generic level only
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
numbers/authors.
|
|
|
|
|
|
|
|
|
|
|
