diff options
| -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] |