From 45e3d2559c4d57a41fe8784dc1a74467b6c6f50a Mon Sep 17 00:00:00 2001
From: Stefan Berghofer
Date: Mon, 3 Feb 2003 09:41:08 +0000
Subject: - 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

---
 isar/isar.el | 24 ++++++++++++++----------
 1 file 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)
-- 
cgit v1.2.3