index
:
proof-general
master
Emacs interface for proof assistants
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
isar
Commit message (
Expand
)
Author
Age
*
Comment unused function
David Aspinall
2007-12-09
*
clarify that -U now defaults to true;
Makarius Wenzel
2007-11-20
*
command 'thm' makes no sense outside a proper context;
Makarius Wenzel
2007-11-13
*
Versions
David Aspinall
2007-11-12
*
proof-shell-issue-pgip-cmd is always isabelle-process-pgip;
Makarius Wenzel
2007-10-24
*
removed obsolete isabelle-version-string, isa-version, isa-supports-pgip;
Makarius Wenzel
2007-10-24
*
isar-find-and-forget: no special treatment of begin/end, just plain undo
Makarius Wenzel
2007-10-18
*
isar-undo-fail-regexp: only isar-keywords-control, not isar-keywords-theory-end;
Makarius Wenzel
2007-10-18
*
allow more specials: oct 327 .. oct 340;
Makarius Wenzel
2007-09-07
*
isar-output-font-lock-keywords-1: hilite markup uses proof-warning-face;
Makarius Wenzel
2007-09-07
*
pg-topterm-regexp: use special 376. isar-goalhyplit-test: Delete closing mark...
David Aspinall
2007-08-19
*
removed outated comment;
Makarius Wenzel
2007-08-15
*
isar-goalhyplit-test: explicit end-marker;
Makarius Wenzel
2007-08-15
*
Add support for sending back literal commands reusing PBP markup mechanisms.
David Aspinall
2007-08-14
*
isar-improper-regexp: include "prems";
Makarius Wenzel
2007-06-14
*
single-char-regexp: tuned symbol regexp;
Makarius Wenzel
2007-06-14
*
isar-font-lock-local: tuned symbol regexp;
Makarius Wenzel
2007-06-14
*
reverted find theorems default from form to minibuffer
weber
2007-06-11
*
XEmacs 21.4.15 does not seem to know propertize
weber
2007-05-17
*
Fix rename
weber
2007-05-11
*
Fix rename
weber
2007-05-11
*
works with XEmacs now (ticket #115)
weber
2007-05-11
*
Fix rename
David Aspinall
2007-05-11
*
Rename [proof]find-theorems -> isar-find-theorems
David Aspinall
2007-05-11
*
Renamed file
David Aspinall
2007-05-11
*
Add experimental find theorems form (not working on all Emacs yet)
David Aspinall
2007-05-10
*
New files.
David Aspinall
2007-05-10
*
x-symbol-isabelle-font-lock-regexp: demand subsequent non-space character;
Makarius Wenzel
2007-05-08
*
undo: removed confusing comment;
Makarius Wenzel
2007-05-08
*
tuned cannot-undo;
Makarius Wenzel
2007-05-08
*
added isar-cmd-sledgehammer;
Makarius Wenzel
2007-05-08
*
tuned pg-special-char-regexp;
Makarius Wenzel
2007-05-08
*
Patch for XEmacs 21.5 beta match-replace bug
David Aspinall
2007-03-03
*
Fix comment
David Aspinall
2007-02-28
*
Comment about undo; use
David Aspinall
2007-01-10
*
tuned;
Makarius Wenzel
2006-12-30
*
back again for isar;
Makarius Wenzel
2006-12-07
*
isar-keywords-theory-enclose: isar-keywords-theory-switch is back again (in p...
Makarius Wenzel
2006-12-07
*
removed obsolete references to 'isa';
Makarius Wenzel
2006-12-07
*
proof-shell-pre-interrupt-hook: removed obsolete Poly/ML 3 setup, which break...
Makarius Wenzel
2006-12-07
*
X-Symbol config. Moved from isa/
David Aspinall
2006-12-05
*
Use Isar-specific isabelle-system file
David Aspinall
2006-12-05
*
isar-keywords-theory-enclose: removed isar-keywords-theory-switch, which usua...
Makarius Wenzel
2006-11-04
*
isar-strip-terminators, isar-detect-begin: proof-search-forward;
Makarius Wenzel
2006-11-04
*
reintroduced pg-subterm-first-special-char, which makes PG strip goal markup;
Makarius Wenzel
2006-10-11
*
isar-keywords-indent-enclose: include "begin" keyword;
Makarius Wenzel
2006-10-11
*
added regexps for begin/end and theory start;
Makarius Wenzel
2006-10-11
*
removed obsolete isar-detect-header;
Makarius Wenzel
2006-10-11
*
isar-goals-font-lock-keywords: added abbreviations;
Makarius Wenzel
2006-08-16
*
Changed the type of proof-goal-command-p. It takes now a span, which
Pierre Courtieu
2006-04-26
[next]