blob: a6c5ca718200c9d91a74804e483ee460b5e555a3 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
|
;; hol98.el Basic Proof General instance for HOL 98
;;
;; Copyright (C) 2000 LFCS Edinburgh.
;;
;; Author: David Aspinall <da@dcs.ed.ac.uk>
;;
;; $Id$
;;
;; Needs improvement!
;;
;; See the README file in this directory for information.
;; keywords:
;; val prove store_thm prove by
;; tacticals: THEN THENL
;; by seems to be "e";
(require 'proof-easy-config) ; easy configure mechanism
(require 'proof-syntax)
(proof-easy-config 'hol98 "HOL"
proof-prog-name "hol.unquote"
proof-terminal-char ?\;
proof-comment-start "(*"
proof-comment-end "*)"
proof-goal-command-regexp "^g[ `]"
proof-save-command-regexp "^qed"
proof-goal-with-hole-regexp "qed_goal \"\\(\\(.*\\)\\)\""
proof-save-with-hole-regexp "qed \"\\(\\(.*\\)\\)\""
proof-non-undoables-regexp "b()"
proof-goal-command "g `%s`;"
proof-save-command "val %s = top_thm(); drop();"
proof-kill-goal-command "drop();"
proof-showproof-command "p()"
proof-undo-n-times-cmd "(pg_repeat backup %s; p());"
proof-auto-multiple-files t
; proof-shell-cd-cmd "cd \"%s\""
proof-shell-prompt-pattern "^[->] "
proof-shell-interrupt-regexp "Interrupted"
; proof-shell-start-goals-regexp "Proof manager status\\|OK.."
proof-shell-start-goals-regexp
(proof-regexp-alt "Proof manager status" "OK.." "val it =\n")
proof-shell-end-goals-regexp
(proof-regexp-alt "^[ \t]*: GoalstackPure.goalstack"
"^[ \t]*: GoalstackPure.proofs")
proof-shell-quit-cmd "quit();"
proof-assistant-home-page
"http://www.cl.cam.ac.uk/Research/HVG/HOL/HOL.html"
proof-shell-annotated-prompt-regexp
"^\\(> val it = () : unit\n\\)?- "
proof-shell-error-regexp "^! "
proof-shell-init-cmd
"Help.displayLines:=3000;
fun pg_repeat f 0 = () | pg_repeat f n = (f(); pg_repeat f (n-1));"
;; FIXME: add optional help topic parameter to help command.
;; Have patch ready for PG 3.2, but PG 3.1 is strictly bug fix.
proof-info-command "help \"hol\""
proof-shell-proof-completed-regexp
"\\(\\(.\\|\n\\)*No subgoals!\n\\)"
; proof-shell-eager-annotation-start
proof-find-theorems-command "DB.match [] (%s);"
;; We must set this to use ptys since mosml doesn't flush its output
;; (on Linux, presumably on Solaris to).
proof-shell-process-connection-type t
)
(provide 'demoisa)
|
