aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2001-08-31UpdatedDavid Aspinall
2001-08-31Move theorem dependency code into proof-depends.el.David Aspinall
2001-08-31Added copy command, call to dependency menu if proof-depends is loaded.David Aspinall
2001-08-31Add simulations of more qed commands, also sort and uniquify dependencies.David Aspinall
2001-08-31Add new proof-mouse-highlight-face to use instead of default. Fix dependency...David Aspinall
2001-08-31new commands (proof terms, code generator);Makarius Wenzel
2001-08-31Remove duplicate entriesDavid Aspinall
2001-08-31Add faces for theorem dependencies.David Aspinall
2001-08-31ExplanationDavid Aspinall
2001-08-31Add DvO to listDavid Aspinall
2001-08-31Add Christophe to listDavid Aspinall
2001-08-31Add auto-compile-vos experimental setting for automatic multiple files.David Aspinall
2001-08-31Remove minibuffer bugDavid Aspinall
2001-08-31Fix for names of functions in proof-dependsDavid Aspinall
2001-08-31Add setting for turning on theorem dependency trackingDavid Aspinall
2001-08-31Update for Isabelle99-2David Aspinall
2001-08-31Clean up of proof-dependsDavid Aspinall
2001-08-31Skip settings which have no PA command in proof-assistant-settings-cmdDavid Aspinall
2001-08-31Add proof-shell-kill-function-hooksDavid Aspinall
2001-08-30include ISABELLE_HOME_USER/etc/isar-keywords.el orMakarius Wenzel
2001-08-30updated;Makarius Wenzel
2001-08-30pg-add-proof-element: removed accidential (?) dynamic scoping onMakarius Wenzel
2001-08-30added proof-script-integral-proofs ("Whether the complete text after aMakarius Wenzel
2001-08-30proof-script-integral-proofs t;Makarius Wenzel
2001-08-30Updated.David Aspinall
2001-08-30Clarify 6.3.1 for multi fileDavid Aspinall
2001-08-30Fix interrupt hook for PolyML 4 in recent IsabelleDavid Aspinall
2001-08-30Set version tag for new release.David Aspinall
2001-08-30Add reassurance to interrupt warning to make Markus happier.David Aspinall
2001-08-30Note about XEmacs 21 and x-symbolDavid Aspinall
2001-08-30Set proof-shell-pre-interrupt-hook for PolyML (not just PolyML 3).David Aspinall
2001-08-30More about invisible proofs and multiple files in Coq. X-symbol compatDavid Aspinall
2001-08-30Updates for recent version of X-symbol, which has no file called x-symbol-aut...David Aspinall
2001-08-30Add :eval form for defpacustom to define PA-specific PG settings as well as P...David Aspinall
2001-08-30Add variable proof-previous-script-bufferDavid Aspinall
2001-08-30fixes for FSF Emacs for searching for goal span (don't call goal-command-p on...David Aspinall
2001-08-30Added implementation of remassq for FSF EmacsDavid Aspinall
2001-08-30pg-insert-last-output-as-comment strips special annotations from last output ...David Aspinall
2001-08-28Fix web page for kitDavid Aspinall
2001-08-28added something in the doc about coq-version-is-V7.Pierre Courtieu
2001-08-28Added something in the doc about coq-version-is-V7, and made the setting ofPierre Courtieu
2001-08-28Updated.David Aspinall
2001-08-28Set version tag for new release.David Aspinall
2001-08-28Change of proof span type back to goalsave fixDavid Aspinall
2001-08-28Change of proof span type back to goalsaveDavid Aspinall
2001-08-28Remove dependent setting of timeout, since bin calls different fn now.David Aspinall
2001-08-28Call function which always waits to prevent odd mode selection bug.David Aspinall
2001-08-28TrivialDavid Aspinall
2001-08-28Remove mention of toolbar variable. Make timeouts vary according to how star...David Aspinall
2001-08-28Timeout happens as intended now, while loading some parts of PG.David Aspinall