From d4d40c64add9a38061ca4958097e96cc2237f040 Mon Sep 17 00:00:00 2001 From: David Aspinall Date: Wed, 8 Feb 2012 17:41:46 +0000 Subject: Fix pareno --- hol-light/hol-light.el | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) (limited to 'hol-light') 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) -- cgit v1.2.3