diff options
| author | Makarius Wenzel | 2005-05-22 17:15:44 +0000 |
|---|---|---|
| committer | Makarius Wenzel | 2005-05-22 17:15:44 +0000 |
| commit | 62116f6ce13c6a670f0ce23b335ab413633d1c63 (patch) | |
| tree | a00885167881fde89b1684eb1a53acb8d622e0d1 | |
| parent | c8a0872fe1ea8cbd0169c96a5794dce5133851c4 (diff) | |
removed find_rwrites, print_intros;
| -rw-r--r-- | isar/isar.el | 13 |
1 files changed, 0 insertions, 13 deletions
diff --git a/isar/isar.el b/isar/isar.el index 523cab31..7f24ba38 100644 --- a/isar/isar.el +++ b/isar/isar.el @@ -352,16 +352,6 @@ proof-shell-retract-files-regexp." ;;; help menu ;;; -(setq find-rewrites-command "find_rewrites \"%s\"") - -(proof-define-assistant-command-witharg isar-help-rewrites - "Search for rewrite rules matching given term." - find-rewrites-command - "Find rewrite rules matching" - (proof-shell-invisible-command arg)) - -(define-key (proof-ass keymap) [h R] 'isar-help-rewrites) - ;;; da: how about a `C-c C-a h ?' for listing available keys? ;;; NB: definvisible must come after derived modes because uses @@ -374,7 +364,6 @@ proof-shell-retract-files-regexp." (proof-definvisible isar-help-facts "print_facts" [h f]) (proof-definvisible isar-help-syntax "print_syntax" [h i]) (proof-definvisible isar-help-induct-rules "print_induct_rules" [h I]) -(proof-definvisible isar-help-intro-rules "print_intros" [h r]) (proof-definvisible isar-help-methods "print_methods" [h m]) (proof-definvisible isar-help-simpset "print_simpset" [h S]) (proof-definvisible isar-help-binds "print_binds" [h b]) @@ -403,8 +392,6 @@ proof-shell-retract-files-regexp." (list ["cases" isar-help-cases t] ["facts" isar-help-facts t] - ["matching rules" isar-help-intro-rules t] - ["matching rewrites" isar-help-rewrites t] ["term bindings" isar-help-binds t] "----" ["classical rules" isar-help-claset t] |