added Isar.init_point, Isar.kill;

--- a/src/Pure/Isar/isar_syn.ML	Thu Jul 10 20:02:55 2008 +0200
+++ b/src/Pure/Isar/isar_syn.ML	Thu Jul 10 20:03:28 2008 +0200
@@ -740,15 +740,23 @@
 (* global Isar state commands *)
 
 val _ =
-  OuterSyntax.improper_command "Isar.linear_undo" "undo tty commands" K.control
+  OuterSyntax.improper_command "Isar.init_point" "init command point-of-interest" K.control
+    (Scan.succeed (Toplevel.no_timing o Toplevel.imperative Isar.init_point));
+
+val _ =
+  OuterSyntax.improper_command "Isar.linear_undo" "undo commands" K.control
     (Scan.optional P.nat 1 >>
       (fn n => Toplevel.no_timing o Toplevel.imperative (fn () => Isar.linear_undo n)));
 
 val _ =
-  OuterSyntax.improper_command "Isar.undo" "undo tty commands (skipping closed proofs)" K.control
+  OuterSyntax.improper_command "Isar.undo" "undo commands (skipping closed proofs)" K.control
     (Scan.optional P.nat 1 >>
       (fn n => Toplevel.no_timing o Toplevel.imperative (fn () => Isar.undo n)));
 
+val _ =
+  OuterSyntax.improper_command "Isar.kill" "kill partial proof or theory development" K.control
+    (Scan.succeed (Toplevel.no_timing o Toplevel.imperative Isar.kill));
+
 
 
 (** diagnostic commands (for interactive mode only) **)