| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 1999-05-27 | renamed undos to undos_proof; | Makarius Wenzel | |
| 1999-05-27 | be chatty; | Makarius Wenzel | |
| 1999-05-27 | proof-parse-to-point improved to support proof-string-start-regexp, | Makarius Wenzel | |
| proof-string-end-regexp, proof-comment-end, proof-comment-start, and parentheses according to current syntax table; renamed proof-commands-regexp to proof-indent-commands-regexp, which is less confusing); | |||
| 1999-05-27 | renamed proof-commands-regexp to proof-indent-commands-regexp, which | Makarius Wenzel | |
| is less confusing); | |||
| 1999-05-27 | improved proof-segment-up-to to support proof-string-start-regexp, | Makarius Wenzel | |
| proof-string-end-regexp; | |||
| 1999-05-27 | added proof-string-start-regexp, proof-string-end-regexp; | Makarius Wenzel | |
| 1999-05-26 | proper setup for indentation; | Makarius Wenzel | |
| improved cannot-undo; | |||
| 1999-05-26 | tuned keywords; | Makarius Wenzel | |
| 1999-05-26 | added isar-keywords-qed-block; | Makarius Wenzel | |
| 1999-05-26 | fixed bug in proof-parse-to-point: missing (setq stack ...) in case of | Makarius Wenzel | |
| closing a proof command; | |||
| 1999-05-26 | closed string in comment; | Makarius Wenzel | |
| 1999-05-25 | more examples; | Makarius Wenzel | |
| 1999-05-25 | removed superficial space; | Makarius Wenzel | |
| 1999-05-25 | added proof-really-save-command-p to support | Makarius Wenzel | |
| more general qed schemes, such as Isabelle/Isar's nested proofs; | |||
| 1999-05-25 | proof-done-advancing: added proof-really-save-command-p to support | Makarius Wenzel | |
| more general qed schemes, such as Isabelle/Isar's nested proofs; | |||
| 1999-05-25 | tuned; | Makarius Wenzel | |
| 1999-05-24 | this version actually generated by Isabelle; | Makarius Wenzel | |
| 1999-05-23 | replaced isar-keywords-section by isar-keywords-theory-heading; | Makarius Wenzel | |
| added isar-not-undoable-commands-regexp; improved isar-cound-undos; proper version of isar-find-and-forget (handles local qeds properly); improved character syntax classes; | |||
| 1999-05-23 | improved classification of keywords (see also isar-keywords.el); | Makarius Wenzel | |
| improved regexps and font-lock; | |||
| 1999-05-23 | Isabelle/Isar keyword classification (used to be in isar-syntax.el); | Makarius Wenzel | |
| 1999-05-23 | tuned usage; | Makarius Wenzel | |
| do not append '/' to PROOFGENERAL_HOME; | |||
| 1999-05-21 | tuned; | Makarius Wenzel | |
| improved isar-find-and-forget; | |||
| 1999-05-21 | tuned -- still quite unsatisfactory; | Makarius Wenzel | |
| 1999-05-21 | made part of the Isabelle sources; | Makarius Wenzel | |
| 1999-05-17 | I've added the custom option 'prog-name-guess' in the generic part and | Patrick Loiseleur | |
| 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 | |||
| 1999-05-17 | several additions, as usual | Patrick Loiseleur | |
| 1999-05-12 | changed use of proof-send (OLD) to proof-shell-insert | Paul Callaghan | |
| 1999-05-11 | instantiation for "plastic" proof assistant | Paul Callaghan | |
| based on the lego instantiation. | |||
| 1999-05-11 | added proof system "plastic", triggered by a .lf extension | Paul Callaghan | |
| 1999-05-11 | Add toggle for proof toolbar to menu | David Aspinall | |
| 1999-05-11 | todo for reorganizing menus. | David Aspinall | |
| 1999-05-03 | *** empty log message *** | Patrick Loiseleur | |
| 1999-05-03 | OrElse -> Orelse | Patrick Loiseleur | |
| 1999-05-03 | proof-home-directory is correct even if $PROOFGENERAL_HOME does not | Patrick Loiseleur | |
| end with a slash. Moreover, the closure proof-home-directory-fn is added so that this value is not computed at compilation time. | |||
| 1999-05-03 | proof-list-global is disabled (must be rewritten) | Patrick Loiseleur | |
| 1999-04-27 | fixed proof-shell-quit-cmd; | Makarius Wenzel | |
| 1999-04-27 | deactivated '.' and '..' keywords (tmp); | Makarius Wenzel | |
| 1999-04-23 | added "thus", "hence"; | Makarius Wenzel | |
| tuned "next"; | |||
| 1999-04-20 | Added the correct proof-shell-restart-cmd | Patrick Loiseleur | |
| 1999-04-20 | A few coloring tricks | Patrick Loiseleur | |
| 1999-04-16 | initial version of 'isar proof assistant (Isabelle/Isar); | Makarius Wenzel | |
| 1999-04-16 | added 'isar proof assistant; | Makarius Wenzel | |
| 1999-04-07 | Set version tag for new release. | proofgen | |
| 1999-04-07 | Merged changes sent by Patrick Loiseleur. | David Aspinall | |
| 1999-03-08 | Fixed. | David Aspinall | |
| 1999-03-08 | Clarification on isa-thy fix. | David Aspinall | |
| 1999-03-08 | Idea for proof-auto-retract, notes about proof-strict-read-only | David Aspinall | |
| 1999-02-24 | Improved documentation on tags | Thomas Kleymann | |
| o added a suggestion by hht o documentation now at generic level only | |||
| 1999-02-23 | extended section on Coq tags | Thomas Kleymann | |
| 1999-02-22 | Set version tag for new release. | David Aspinall | |
 |
index : proof-general | |
| Emacs plugins for proof management systems |
| aboutsummaryrefslogtreecommitdiff |