;; isa-mode.el Emacs support for Isabelle proof assistant ;; Copyright (C) 1993-2000 LFCS Edinburgh, David Aspinall. ;; ;; Author: David Aspinall ;; Maintainer: Proof General maintainer ;; ;; $Id$ ;; ;; ----------------------------------------------------------------- ;; ;; This file and the rest of Isabelle Proof General contain code taken ;; from David Aspinall's Isamode system, a personal project undertaken ;; 1993-1999 as a contribution to the Isabelle community. ;; ;; ----------------------------------------------------------------- ;; Add Isabelle image onto splash screen ;; (customize-set-variable 'proof-splash-extensions '(list nil (proof-splash-display-image "isabelle_transparent" t))) ;; In case Isa mode was invoked directly or by -*- isa -*- at ;; the start of the file, ensure that Isa mode is used from now ;; on for .thy and .ML files. ;; FIXME: be less messy with auto-mode-alist here (remove dups) (setq auto-mode-alist (cons '("\\.ML$\\|\\.thy$" . isa-mode) auto-mode-alist)) (require 'proof) (require 'isa-syntax) (require 'isabelle-system) ;;; ;;; ======== User settings for Isabelle ======== ;;; ;;; proof-site provides us with the cusomization groups ;;; ;;; 'isabelle - User options for Isabelle Proof General ;;; 'isabelle-config - Configuration of Isabelle Proof General ;;; (constants, but may be nice to tweak) ;;; ;;; ======== Configuration of generic modes ======== ;;; (defcustom isa-outline-regexp (proof-ids-to-regexp '("goal" "Goal" "prove_goal")) "Outline regexp for Isabelle ML files" :type 'regexp :group 'isabelle-config) ;;; End of a command needs parsing to find, so this is approximate. (defcustom isa-outline-heading-end-regexp ";[ \t\n]*" "Outline heading end regexp for Isabelle ML files." :type 'regexp :group 'isabelle-config) (defvar isa-shell-outline-regexp "\370[ \t]*\\([0-9]+\\)\\.") (defvar isa-shell-outline-heading-end-regexp "$") (defun isa-mode-config-set-variables () "Configure generic proof scripting/thy mode variables for Isabelle. Settings here are the ones which are needed for both shell mode and script mode." (setq proof-assistant-home-page isabelle-web-page proof-mode-for-script 'isa-proofscript-mode ;; proof script syntax proof-terminal-char ?\; ; ends a proof proof-comment-start "(*" ; comment in a proof proof-comment-end "*)" ; ;; Next few used for func-menu and recognizing goal..save regions in ;; script buffer. proof-save-command-regexp isa-save-command-regexp proof-goal-command-regexp isa-goal-command-regexp proof-goal-with-hole-regexp isa-goal-with-hole-regexp proof-save-with-hole-regexp isa-save-with-hole-regexp ;; Unfortunately the default value of proof-script-next-entity-regexps ;; is no good, because goals with holes in Isabelle are batch ;; commands, and not terminated by saves. So we omit the forward ;; search from the default value. proof-script-next-entity-regexps (list (proof-regexp-alt isa-goal-with-hole-regexp isa-save-with-hole-regexp) (list isa-goal-with-hole-regexp 2) (list isa-save-with-hole-regexp 2 'backward isa-goal-command-regexp)) proof-indent-enclose-offset (- proof-indent) proof-indent-open-offset 0 proof-indent-close-offset 0 proof-indent-any-regexp isa-indent-any-regexp proof-indent-inner-regexp isa-indent-inner-regexp proof-indent-enclose-regexp isa-indent-enclose-regexp proof-indent-open-regexp isa-indent-open-regexp proof-indent-close-regexp isa-indent-close-regexp ;; proof engine commands proof-showproof-command "pr();" proof-goal-command "Goal \"%s\";" proof-save-command "qed \"%s\";" proof-context-command "ProofGeneral.show_context();" proof-info-command "ProofGeneral.help();" proof-kill-goal-command "ProofGeneral.kill_goal();" proof-find-theorems-command "ProofGeneral.thms_containing (space_explode \",\" \"%s\");" proof-shell-start-silent-cmd "Goals.disable_pr();" proof-shell-stop-silent-cmd "Goals.enable_pr();" ;; command hooks proof-goal-command-p 'isa-goal-command-p proof-count-undos-fn 'isa-count-undos proof-find-and-forget-fn 'isa-find-and-forget proof-state-preserving-p 'isa-state-preserving-p ;; close goal..save regions eagerly proof-completed-proof-behaviour 'closeany proof-shell-compute-new-files-list 'isa-shell-compute-new-files-list proof-shell-inform-file-processed-cmd "ProofGeneral.inform_file_processed \"%s\";" proof-shell-inform-file-retracted-cmd "ProofGeneral.inform_file_retracted \"%s\";" ;; Parsing error messages. Bit tricky to allow for ;; multitude of possible error formats Isabelle spits out. ;; Ideally we shouldn't bother parsing errors that appear ;; in the temporary ML files generated while reading ;; theories, but unfortunately the user sometimes needs to ;; examine them to understand a strange problem... proof-shell-next-error-regexp "\\(error on \\|Error: in '[^']+', \\)line \\([0-9]+\\)\\|The error(s) above occurred" proof-shell-next-error-filename-regexp "\\(Loading theory \"\\|Error: in '\\)\\([^\"']+\\)[\"']" proof-shell-next-error-extract-filename "%s.thy")) (defun isa-shell-mode-config-set-variables () "Configure generic proof shell mode variables for Isabelle." (setq proof-shell-first-special-char ?\350 proof-shell-wakeup-char ?\372 proof-shell-annotated-prompt-regexp "\\(val it = () : unit\n\\)?> \372" ;; This pattern is just for comint proof-shell-prompt-pattern "^2?[ML-=#>]>? \372?" ;; for issuing command, not used to track cwd in any way. proof-shell-cd-cmd "ThyLoad.add_path \"%s\";" ;; Escapes for filenames inside ML strings. ;; We also make a hack for Isabelle, by switching from backslashes ;; to forward slashes if it looks like we're running on Windows. proof-shell-filename-escapes (if (fboundp 'win32-long-file-name) ; rough test for XEmacs on win32 ;; Patterns to unixfy names. Avoids a deliberate bomb in Isabelle which ;; barfs at paths with these characters in them. '(("\\\\" . "/") ("\"" . "\\\"") ("^[a-zA-Z]:" . "")) ;; Normal case: quotation for backslash, quote mark. '(("\\\\" . "\\\\") ("\"" . "\\\""))) proof-shell-interrupt-regexp "Interrupt" proof-shell-error-regexp "^\364\\*\\*\\*\\|^.*Error:\\|^uncaught exception \\|^Exception-\\( \\|$\\)" ;; matches names of assumptions proof-shell-assumption-regexp isa-id ;; matches subgoal name ;; FIXME: not used yet. In future will be used for ;; proof-by-pointing like features. ;; proof-shell-goal-regexp "\370[ \t]*\\([0-9]+\\)\\." proof-shell-start-goals-regexp "\366" proof-shell-end-goals-regexp "\367" proof-shell-goal-char ?\370 proof-shell-proof-completed-regexp "^No subgoals!" ;; initial command configures Isabelle by hacking print functions, ;; restoring settings saved by Proof General, etc. ;; FIXME: temporary hack for almost enabling/disabling printing. ;; Also for setting default values. proof-shell-pre-sync-init-cmd "ProofGeneral.init false;" proof-shell-init-cmd (proof-assistant-settings-cmd) proof-shell-restart-cmd "ProofGeneral.isa_restart();" proof-shell-quit-cmd "quit();" proof-shell-eager-annotation-start "\360\\|\362" proof-shell-eager-annotation-start-length 1 proof-shell-eager-annotation-end "\361\\|\363" ;; Some messages delimited by eager annotations proof-shell-clear-response-regexp "Proof General, please clear the response buffer." proof-shell-clear-goals-regexp "Proof General, please clear the goals buffer." proof-shell-set-elisp-variable-regexp "Proof General, please set the variable \\([^ ]+\\) to: #\\([^#]+\\)#\\." proof-shell-theorem-dependency-list-regexp "Proof General, the theorem dependencies are: \"\\([^\"]*\\)\"" ;; Dirty hack to allow font-locking for output based on hidden ;; annotations, see isa-output-font-lock-keywords-1 proof-shell-leave-annotations-in-output t ;; === ANNOTATIONS === ones here are broken proof-shell-result-start "\372 Pbp result \373" proof-shell-result-end "\372 End Pbp result \373" proof-analyse-using-stack t proof-shell-start-char ?\372 proof-shell-end-char ?\373 proof-shell-field-char ?\374 ;; === MULTIPLE FILE HANDLING === proof-shell-process-file (cons ;; Theory loader output and verbose update() output. "Proof General, this file is loaded: \"\\(.*\\)\"" (lambda (str) (match-string 1 str))) ;; This is the output returned by a special command to ;; query Isabelle for outdated files. ;; proof-shell-clear-included-files-regexp ;; "Proof General, please clear your record of loaded files." proof-shell-retract-files-regexp "Proof General, you can unlock the file \"\\(.*\\)\"" proof-shell-compute-new-files-list 'isa-shell-compute-new-files-list ) (add-hook 'proof-activate-scripting-hook 'isa-shell-update-thy 'append) ) ;;; ;;; Theory loader operations ;;; ;; Experiments for background non-blocking loading of theory: this is ;; quite difficult, actually: we need to set a callback from ;; proof-done-invisible to take the final step in switching on ;; scripting. We may be able to pass the hook argument into the ;; action list using the "span" argument which means nothing for ;; invisible command usually. ; attempt to trap C-g. Needs more work so revert to previous ;(defun isa-update-thy-only (file try wait) ; "Tell Isabelle to update current buffer's theory, and all ancestors." ; ;; Trap interrupts from C-g during the update ; (condition-case err ; (proof-shell-invisible-command ; (format "ProofGeneral.%supdate_thy_only \"%s\";" ; (if try "try_" "") (file-name-sans-extension file)) ; wait) ; (t (message "Isabelle Proof General: error or interrupt during update theory...") ; (if proof-shell-busy ; (proof-interrupt-process)) ; (sit-for 1) ; (proof-deactivate-scripting) ; (if (cdr err) ;; quit is just (quit). ; (error (cdr err)))))) (defun isa-update-thy-only (file try wait) "Tell Isabelle to update current buffer's theory, and all ancestors." ;; First make sure we're in the right directory to take care of ;; relative "files" paths inside theory file. (proof-cd-sync) (proof-shell-invisible-command (proof-format-filename ;; %r parameter means relative (don't expand) path (format "ProofGeneral.%supdate_thy_only \"%%r\";" (if try "try_" "")) (file-name-nondirectory (file-name-sans-extension file))) wait)) (defun isa-shell-update-thy () "Possibly issue update_thy_only command to Isabelle. If the current buffer has an empty locked region, the interface is about to send commands from it to Isabelle. This function sends a command to read any theory file corresponding to the current ML file. This is a hook function for proof-activate-scripting-hook." (if (proof-locked-region-empty-p) ;; If we switch to this buffer and it *does* have a locked ;; region, we could check that no updates are needed and ;; unlock the whole buffer in case they were. But that's ;; a bit messy. Instead we assume that things must be ;; up to date, after all, the user wasn't allowed to edit ;; anything that this file depends on, was she? (progn ;; Wait after sending, so that queue is cleared for further ;; commands without giving "proof process busy" error. (isa-update-thy-only buffer-file-name t ;; whether to block or not (if (and (boundp 'activated-interactively) activated-interactively) t ; was nil, but falsely leaves Scripting on! t)) ;; Leave the messages from the update around. (setq proof-shell-erase-response-flag nil)))) (defun isa-remove-file (name files cmp-base) (if (not files) nil (let* ((file (car files)) (rest (cdr files)) (same (if cmp-base (string= name (file-name-nondirectory file)) (string= name file)))) (if same (isa-remove-file name rest cmp-base) (cons file (isa-remove-file name rest cmp-base)))))) (defun isa-shell-compute-new-files-list (str) "Compute the new list of files read by the proof assistant. This is called when Proof General spots output matching proof-shell-retract-files-regexp." (let* ((name (match-string 1 str)) (base-name (file-name-nondirectory name))) (if (string= name base-name) (isa-remove-file name proof-included-files-list t) (isa-remove-file (file-truename name) proof-included-files-list nil)))) ;; ;; Define the derived modes ;; (eval-and-compile (define-derived-mode isa-shell-mode proof-shell-mode "Isabelle shell" nil (isa-shell-mode-config))) (eval-and-compile (define-derived-mode isa-response-mode proof-response-mode "Isabelle response" nil (isa-response-mode-config))) (eval-and-compile ; to define vars for byte comp. (define-derived-mode isa-goals-mode proof-goals-mode "Isabelle goals" nil (isa-goals-mode-config))) (eval-and-compile ; to define vars for byte comp. (define-derived-mode isa-proofscript-mode proof-mode "Isabelle script" nil (isa-mode-config))) ;; ;; Automatically selecting theory mode or Proof General script mode. ;; (defun isa-mode () "Mode for Isabelle buffers: either isa-proofscript-mode or thy-mode. Files with extension .thy will be in thy-mode, otherwise we choose isa-proofscript-mode." (interactive) (cond (;; Theory files only if they have the right extension (and (buffer-file-name) (string-match "\\.thy$" (buffer-file-name))) ;; Enter theory mode, but first configure settings for proof ;; script if they haven't been done already. This is a hack, ;; needed because Proof General assumes that the script mode must ;; have been configured before shell mode can be triggered, which ;; isn't true for Isabelle. ;; (proof-config-done-related and proof-shell-mode refer to ;; the troublesome settings in question) (unless proof-terminal-char (isa-mode-config-set-variables)) (thy-mode) ;; related mode configuration including locking buffer, ;; fontification, etc. (proof-config-done-related) ;; Hack for splash screen (if (and (boundp 'proof-mode-hook) (memq 'proof-splash-timeout-waiter proof-mode-hook)) (proof-splash-timeout-waiter) ;; Otherwise, user may need welcoming. (proof-splash-message))) (t (isa-proofscript-mode)))) (eval-after-load "thy-mode" ;; Extend theory mode keymap '(let ((map thy-mode-map)) (define-key map "\C-c\C-b" 'isa-process-thy-file) (define-key map "\C-c\C-r" 'isa-retract-thy-file) (proof-define-keys map proof-universal-keys))) ;; FIXME: could test that the buffer isn't already locked. (defun isa-process-thy-file (file) "Process the theory file FILE. If interactive, use buffer-file-name." (interactive (list buffer-file-name)) (save-some-buffers) (isa-update-thy-only file nil nil)) (defcustom isa-retract-thy-file-command "ThyInfo.remove_thy \"%r\";" "Sent to Isabelle to forget theory file and descendants. Resulting output from Isabelle will be parsed by Proof General." :type 'string :group 'isabelle-config) (defun isa-retract-thy-file (file) "Retract the theory file FILE. If interactive, use buffer-file-name. To prevent inconsistencies, scripting is deactivated before doing this. So if scripting is active in an ML file which is not completely processed, you will be asked to retract the file or process the remainder of it." (interactive (list buffer-file-name)) (proof-deactivate-scripting) (proof-shell-invisible-command (proof-format-filename isa-retract-thy-file-command (file-name-nondirectory (file-name-sans-extension file))))) ;; Next bits taken from isa-load.el ;; isa-load.el,v 3.8 1998/09/01 (defgroup thy nil "Customization of Isamode's theory editing mode" ;; :link '(info-link "(Isamode)Theory Files") :load 'thy-mode :group 'isabelle) (autoload 'thy-mode "thy-mode" "Major mode for Isabelle theory files" t nil) (autoload 'thy-find-other-file "thy-mode" "Find associated .ML or .thy file." t nil) (defun isa-splice-separator (sep strings) (let (stringsep) (while strings (setq stringsep (concat stringsep (car strings))) (setq strings (cdr strings)) (if strings (setq stringsep (concat stringsep sep)))) stringsep)) (defun isa-file-name-cons-extension (name) "Return cons cell of NAME without final extension and extension" (if (string-match "\\.[^\\.]+$" name) (cons (substring name 0 (match-beginning 0)) (substring name (match-beginning 0))) (cons name ""))) (defun isa-format (alist string) "Format a string by matching regexps in ALIST against STRING" (while alist (while (string-match (car (car alist)) string) (setq string (concat (substring string 0 (match-beginning 0)) (cdr (car alist)) (substring string (match-end 0))))) (setq alist (cdr alist))) string) ;; Key to switch to theory mode (define-key isa-proofscript-mode-map [(control c) (control o)] 'thy-find-other-file) ;; ;; Code that's Isabelle specific ;; (defcustom isa-not-undoable-commands-regexp (proof-ids-to-regexp '("undo")) "Regular expression matching commands which are *not* undoable." :type 'regexp :group 'isabelle-config) ;; This next function is the important one for undo operations. (defun isa-count-undos (span) "Count number of undos in a span, return the command needed to undo that far." (let ((case-fold-search nil) (ct 0) str i) (if (and span (prev-span span 'type) (not (eq (span-property (prev-span span 'type) 'type) 'comment)) (isa-goal-command-p (span-property (prev-span span 'type) 'cmd))) (concat "choplev 0" proof-terminal-string) (while span (setq str (span-property span 'cmd)) (cond ((eq (span-property span 'type) 'vanilla) (or (proof-string-match isa-not-undoable-commands-regexp str) (setq ct (+ 1 ct)))) ((eq (span-property span 'type) 'pbp) ;; this case probably redundant for Isabelle, unless we ;; think of some nice ways of matching non-undoable cmds. (cond ((not (proof-string-match isa-not-undoable-commands-regexp str)) (setq i 0) (while (< i (length str)) (if (= (aref str i) proof-terminal-char) (setq ct (+ 1 ct))) (setq i (+ 1 i)))) (t nil)))) (setq span (next-span span 'type))) (concat "ProofGeneral.repeat_undo " (int-to-string ct) proof-terminal-string)))) (defun isa-goal-command-p (str) "Decide whether argument is a goal or not" (proof-string-match isa-goal-command-regexp str)) ; this regexp defined in isa-syntax.el ;; Isabelle has no concept of a Linear context, so forgetting back ;; to the declaration of a particular something makes no real ;; sense. Perhaps in the future there will be functions to remove ;; theorems from theories, but even then all we could do is ;; forget particular theorems one by one. So we ought to search ;; backwards in isa-find-and-forget, rather than forwards as ;; the code from the type theory provers does. ;; MMW: this version even does nothing at all (defun isa-find-and-forget (span) proof-no-command) (defun isa-state-preserving-p (cmd) "Non-nil if command preserves the proofstate." (not (proof-string-match isa-not-undoable-commands-regexp cmd))) ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; Isa shell startup and exit hooks ;; ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; (defun isa-pre-shell-start () (setq proof-prog-name (isabelle-command-line)) (setq proof-mode-for-shell 'isa-shell-mode) (setq proof-mode-for-goals 'isa-goals-mode) (setq proof-mode-for-response 'isa-response-mode)) (defun isa-mode-config () (isa-mode-config-set-variables) (isa-init-syntax-table) (setq font-lock-keywords isa-font-lock-keywords-1) (proof-config-done) ;; outline ;; FIXME: do we need to call make-local-variable here? (make-local-variable 'outline-regexp) (setq outline-regexp isa-outline-regexp) (make-local-variable 'outline-heading-end-regexp) (setq outline-heading-end-regexp isa-outline-heading-end-regexp) ;; tags ; (and (boundp 'tag-table-alist) ; (setq tag-table-alist ; (append '(("\\.ML$" . isa-ML-file-tags-table) ; ("\\.thy$" . thy-file-tags-table)) ; tag-table-alist))) (setq blink-matching-paren-dont-ignore-comments t)) ;; These hooks are added on load because proof shells can ;; be started from .thy (not in scripting mode) or .ML files. (add-hook 'proof-pre-shell-start-hook 'isa-pre-shell-start nil t) (add-hook 'proof-shell-insert-hook 'isa-preprocessing) (defun isa-shell-mode-config () "Configure Proof General proof shell for Isabelle." (isa-init-output-syntax-table) (setq font-lock-keywords isa-output-font-lock-keywords-1) (isa-shell-mode-config-set-variables) (proof-shell-config-done)) (defun isa-response-mode-config () (setq font-lock-keywords isa-output-font-lock-keywords-1) (isa-init-output-syntax-table) (proof-response-config-done)) (defun isa-goals-mode-config () ;; FIXME: next two broken, of course, as is PBP everywhere except LEGO. (setq pbp-change-goal "Show %s.") (setq pbp-error-regexp proof-shell-error-regexp) (isa-init-output-syntax-table) (setq font-lock-keywords isa-goals-font-lock-keywords) (proof-goals-config-done)) (defun isa-preprocessing () ;dynamic scoping of `string' "Handle ^VERBATIM marker -- acts on variable STRING by dynamic scoping" (if (string-match isabelle-verbatim-regexp string) (setq string (match-string 1 string)))) ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; ;; x-symbol support for Isabelle PG, provided by David von Oheimb. ;; ;; The following settings configure the generic PG package. ;; The token language "Isabelle Symbols" is in file x-symbol-isa.el ;; (setq proof-xsym-extra-modes '(thy-mode) proof-xsym-activate-command "print_mode := ([\"xsymbols\",\"symbols\"] @ ! print_mode);" proof-xsym-deactivate-command "print_mode := (! print_mode \\\\ [\"xsymbols\",\"symbols\"]);") ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; ;; Completion table for Isabelle identifiers ;; ;; Ideally this could be set automatically from the running process, ;; and maybe a default value could be dumped by Isabelle when it is ;; built. (defpgdefault completion-table '("quit" "cd" "use" "use_thy" "time_use" "time_use_thy" "Pretty.setdepth" "Pretty.setmargin" "print_depth" "show_hyps" "show_types" "show_sorts" "print_exn" "goal" "goalw" "goalw_cterm" "premises" "by" "byev" "result" "uresult" "chop" "choplev" "back" "undo" "pr" "prlev" "goals_limit" "proof_timing" "prove_goal" "prove_goalw" "prove_goalw_cterm" "push_proof" "pop_proof" "rotate_proof" "save_proof" "restore_proof" "read" "prin" "printyp" "topthm" "getgoal" "gethyps" "filter_goal" "compat_goal" ;; short cuts - should these be included? "ba" "br" "be" "bd" "brs" "bes" "bds" "fs" "fr" "fe" "fd" "frs" "fes" "fds" "bw" "bws" "ren" "resolve_tac" "eresolve_tac" "dresolve_tac" "forward_tac" "assume_tac" "eq_assume_tac" "match_tac" "ematch_tac" "dmatch_tac" "res_inst_tac" "eres_inst_tac" "dres_inst_tac" "forw_inst_tac" "rewrite_goals_tac" "rewrite_tac" "fold_goals_tac" "fold_goals_tac" "fold_tac" "cut_facts_tac" "subgoal_tac" ;; short cuts - should these be included? "rtac" "etac" "dtac" "atac" "ares_tac" "rewtac" ;; In general, I think rules should appear in rule tables, not here. "asm_rl" "cut_rl" "flexflex_tac" "rename_tac" "rename_last_tac" "Logic.set_rename_prefix" "Logic.auto_rename" "compose_tac" "biresolve_tac" "bimatch_tac" "subgoals_of_brl" "lessb" "head_string" "insert_thm" "delete_thm" "compat_resolve_tac" "could_unify" "filter_thms" "filt_resolve_tac" ;; probably shouldn't be included: "tapply" "Tactic" "PRIMITIVE" "STATE" "SUBGOAL" "pause_tac" "print_tac" "THEN" "ORELSE" "APPEND" "INTLEAVE" "EVERY" "FIRST" "TRY" "REPEAT_DETERM" "REPEAT" "REPEAT1" "trace_REPEAT" "all_tac" "no_tac" "FILTER" "CHANGED" "DEPTH_FIRST" "DEPTH_SOLVE" "DEPTH_SOLVE_1" "trace_DEPTH_FIRST" "BREADTH_FIRST" "BEST_FIRST" "THEN_BEST_FIRST" "trace_BEST_FIRST" "COND" "IF_UNSOLVED" "DETERM" "SELECT_GOAL" "METAHYPS" "ALLGOALS" "TRYALL" "SOMEGOAL" "FIRSTGOAL" "REPEAT_SOME" "REPEAT_FIRST" "trace_goalno_tac" ;; include primed versions of tacticals? "EVERY1" "FIRST1" "prth" "prths" "prthq" "RSN" "RLN" "RL" ;; simplifier "addsimps" "addeqcongs" "delsimps" "setsolver" "setloop" "setmksimps" "setsubgoaler" "empty_ss" "merge_ss" "prems_of_ss" "rep_ss" "simp_tac" "asm_full_simp_tac" "asm_simp_tac" ;; classical prover "empty_cs" "addDs" "addEs" "addIs" "addSDs" "addSEs" "addSIs" "print_cs" "rep_claset" "best_tac" "chain_tac" "contr_tac" "eq_mp_tac" "fast_tac" "joinrules" "mp_tac" "safe_tac" "safe_step_tac" "slow_best_tac" "slow_tac" "step_tac" "swapify" "swap_res_tac" "inst_step_tac" ;; that's it for now! )) (provide 'isa)