diff options
| author |  David Aspinall <da@inf.ed.ac.uk> | 2012-02-08 17:41:46 +0000 |
|---|---|---|
| committer | David Aspinall <da@inf.ed.ac.uk> | 2012-02-08 17:41:46 +0000 |
| commit | d4d40c64add9a38061ca4958097e96cc2237f040 (patch) | |
| tree | 455a59b9cc54c34a6bdd7202cb60a94d48dd4f98 /hol-light | |
| parent | 06b0e65a5b0a3bd900197af234913d58d4b2c3fc (diff) | |
Fix pareno
Diffstat (limited to 'hol-light')
| -rw-r--r-- | hol-light/hol-light.el | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/hol-light/hol-light.el b/hol-light/hol-light.el index 3ba67eee..4b366f6c 100644 --- a/hol-light/hol-light.el +++ b/hol-light/hol-light.el @@ -60,12 +60,12 @@ You need to restart Emacs if you change this setting." (if hol-light-use-custom-toplevel (list (format "#use \"%shol-light/pg_tactics.ml\"" proof-home-directory)) - (list + (list "let rec pg_repeat f n = match n with 0 -> () | _ -> (f(); pg_repeat f (n-1));;" "let pg_undo n = (pg_repeat n (fun ()->let _ = b() in ()); p());;" "let pg_kill() = current_goalstack:=[];;" - "let pg_forget id = ();;") - "let pg_restart() = print_string \"*** Session restarted.\";;")) + "let pg_forget id = ();;" + "let pg_restart() = print_string \"*** Session restarted.\";;"))) "*Commands used to start up a running HOL Light session." :type '(list string) :group 'hol-light) |