diff options
| author |  Makarius Wenzel <makarius@sketis.net> | 2011-08-31 18:18:21 +0000 |
|---|---|---|
| committer | Makarius Wenzel <makarius@sketis.net> | 2011-08-31 18:18:21 +0000 |
| commit | 2b4eef78f93be6447e63ecb2270f3d798f877225 (patch) | |
| tree | 59c2297b5f0d2d934f59e88ba718a4e3e19b6310 /isar | |
| parent | 5c9346db0592f3b51365bf72f46003bddbaf5398 (diff) | |
clarified isar-improper-regexp -- "prems" is already reported as legacy by the prover (after Isabelle2011);
Diffstat (limited to 'isar')
| -rw-r--r-- | isar/isar-syntax.el | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/isar/isar-syntax.el b/isar/isar-syntax.el index 45ad87f9..340f2e96 100644 --- a/isar/isar-syntax.el +++ b/isar/isar-syntax.el @@ -216,7 +216,7 @@ Group number 1 matches the identifier possibly with quotes; group number 2 matches contents of quotes for quoted identifiers.") (defconst isar-improper-regexp - "\\(\\<[A-Za-z][A-Za-z0-9'_]*_tac\\>\\|\\<goal[0-9]+\\>\\|\\<prems\\>\\)" + "\\(\\<[A-Za-z][A-Za-z0-9'_]*_tac\\>\\|\\<goal[0-9]+\\>\\)" "Regexp matching low-level features") (defconst isar-save-command-regexp |