diff options
| author |  David Aspinall <da@inf.ed.ac.uk> | 2010-08-17 17:17:20 +0000 |
|---|---|---|
| committer | David Aspinall <da@inf.ed.ac.uk> | 2010-08-17 17:17:20 +0000 |
| commit | 4b87261584d27b01e9c3edc749076051f8490a92 (patch) | |
| tree | 37d6b25164045a583be3432aa92c6164ea76c4ac /isar/isar.el | |
| parent | 55d2ef1416207c411e98c57ad7717c1aa7569b50 (diff) | |
Fix key bindings. Ref Trac#334
Diffstat (limited to 'isar/isar.el')
| -rw-r--r-- | isar/isar.el | 28 |
1 files changed, 14 insertions, 14 deletions
diff --git a/isar/isar.el b/isar/isar.el index 92ef0b9d..2ab4ea88 100644 --- a/isar/isar.el +++ b/isar/isar.el @@ -331,19 +331,19 @@ This is called when Proof General spots output matching ;;; NB: definvisible must be after derived modes (uses isar-mode-map) -(proof-definvisible isar-help-antiquotations "print_antiquotations" [h A]) -(proof-definvisible isar-help-attributes "print_attributes" [h a]) -(proof-definvisible isar-help-cases "print_cases" [h c]) -(proof-definvisible isar-help-claset "print_claset" [h C]) -(proof-definvisible isar-help-commands "print_commands" [h o]) -(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-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]) +(proof-definvisible isar-help-antiquotations "print_antiquotations" "hA") +(proof-definvisible isar-help-attributes "print_attributes" "ha") +(proof-definvisible isar-help-cases "print_cases" "hc") +(proof-definvisible isar-help-claset "print_claset" "hC") +(proof-definvisible isar-help-commands "print_commands" "ho") +(proof-definvisible isar-help-facts "print_facts" "hf") +(proof-definvisible isar-help-syntax "print_syntax" "hi") +(proof-definvisible isar-help-induct-rules "print_induct_rules" "hI") +(proof-definvisible isar-help-methods "print_methods" "hm") +(proof-definvisible isar-help-simpset "print_simpset" "hS") +(proof-definvisible isar-help-binds "print_binds" "hb") +(proof-definvisible isar-help-theorems "print_theorems" "ht") +(proof-definvisible isar-help-trans-rules "print_trans_rules" "hT") ;; ;; Command menu @@ -366,7 +366,7 @@ This is called when Proof General spots output matching (proof-definvisible isar-cmd-quickcheck "quickcheck" [(control q)]) (proof-definvisible isar-cmd-nitpick "nitpick" [(control n)]) -(proof-definvisible isar-cmd-refute "refute" [r]) +(proof-definvisible isar-cmd-refute "refute" "r") (proof-definvisible isar-cmd-sledgehammer "sledgehammer" [(control s)]) (defpgdefault menu-entries |