diff options
| author | Stefan Berghofer | 2003-02-03 09:41:08 +0000 |
|---|---|---|
| committer | Stefan Berghofer | 2003-02-03 09:41:08 +0000 |
| commit | 45e3d2559c4d57a41fe8784dc1a74467b6c6f50a (patch) | |
| tree | 498423eb313b5e93af34abf14b1f5a481ff8ee28 | |
| parent | 0a493ccb7ec4906792349744907585de39634698 (diff) | |
- Moved "show me" menu one level up in the menu hierarchy
- Reordered entries in "show me" menu and added entry for displaying matching
introduction rules
| -rw-r--r-- | isar/isar.el | 24 |
1 files changed, 14 insertions, 10 deletions
diff --git a/isar/isar.el b/isar/isar.el index 8902ad49..8d39514d 100644 --- a/isar/isar.el +++ b/isar/isar.el @@ -347,31 +347,35 @@ 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]) (proof-definvisible isar-help-theorems "print_theorems" [h t]) (proof-definvisible isar-help-trans-rules "print_trans_rules" [h T]) -(defpgdefault help-menu-entries +(defpgdefault menu-entries (append - isabelle-docs-menu + (list isabelle-logics-menu) (list (cons "Show me ..." (list - ["antiquotations" isar-help-antiquotations t] - ["attributes" isar-help-attributes t] ["cases" isar-help-cases t] - ["classical rules" isar-help-claset t] - ["commands" isar-help-commands t] ["facts" isar-help-facts t] - ["inner syntax" isar-help-syntax t] + ["matching rules" isar-help-intro-rules t] + ["term bindings" isar-help-binds t] + "----" + ["classical rules" isar-help-claset t] ["induct/cases rules" isar-help-induct-rules t] - ["methods" isar-help-methods t] ["simplifier rules" isar-help-simpset t] - ["term bindings" isar-help-binds t] ["theorems" isar-help-theorems t] - ["transitivity rules" isar-help-trans-rules t]))))) + ["transitivity rules" isar-help-trans-rules t] + "----" + ["antiquotations" isar-help-antiquotations t] + ["attributes" isar-help-attributes t] + ["commands" isar-help-commands t] + ["inner syntax" isar-help-syntax t] + ["methods" isar-help-methods t]))))) ;; undo proof commands (defun isar-count-undos (span) |