src/Pure/Isar/isar_syn.ML

 val _ =
   OuterSyntax.command "end" "end (local) theory" (K.tag_theory K.thy_end)
     (Scan.succeed (Toplevel.exit o Toplevel.end_local_theory));
 
 
+
 (** markup commands **)
 
 val _ = OuterSyntax.markup_command ThyOutput.Markup "header" "theory header" K.diag
   (P.doc_source >> IsarCmd.header_markup);
 

   "raw document preparation text (proof)" (K.tag_proof K.prf_decl)
   (P.doc_source >> IsarCmd.proof_markup);
 
 
 
-(** theory sections **)
+(** theory commands **)
 
 (* classes and sorts *)
 
 val _ =
   OuterSyntax.command "classes" "declare type classes" K.thy_decl

     (calc_args >> (Toplevel.proofs' o Calculation.also));
 
 val _ =
   OuterSyntax.command "finally" "combine calculation and current facts, exhibit result"
     (K.tag_proof K.prf_chain)
-    (calc_args >> (Toplevel.proofs' o Calculation.finally_));
+    (calc_args >> (Toplevel.proofs' o Calculation.finally));
 
 val _ =
   OuterSyntax.command "moreover" "augment calculation by current facts"
     (K.tag_proof K.prf_decl)
     (Scan.succeed (Toplevel.proof' Calculation.moreover));

         [tr] => Scan.succeed (K tr)
       | _ => Scan.fail_with (K "exactly one command expected"))
       handle ERROR msg => Scan.fail_with (K msg)));
 
 
-(* global history commands *)
-
-val _ =
-  OuterSyntax.improper_command "init_toplevel" "init toplevel point-of-interest" K.control
-    (Scan.succeed (Toplevel.no_timing o Toplevel.imperative Isar.init));
-
-val _ =
-  OuterSyntax.improper_command "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 "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 "undos_proof" "undo commands (skipping closed proofs)" K.control
-    (Scan.optional P.nat 1 >> (fn n => Toplevel.no_timing o
-      Toplevel.keep (fn state =>
-        if Toplevel.is_proof state then (Isar.undo n; Isar.print ()) else raise Toplevel.UNDEF)));
-
-val _ =
-  OuterSyntax.improper_command "cannot_undo" "partial undo -- Proof General legacy" K.control
-    (P.name >>
-      (fn "end" => Toplevel.no_timing o Toplevel.imperative (fn () => Isar.undo 1)
-        | txt => Toplevel.imperative (fn () => error ("Cannot undo " ^ quote txt))));
-
-val _ =
-  OuterSyntax.improper_command "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) **)
 
 val opt_modes = Scan.optional (P.$$$ "(" |-- P.!!! (Scan.repeat1 P.xname --| P.$$$ ")")) [];
 val opt_bang = Scan.optional (P.$$$ "!" >> K true) false;

     K.diag (Scan.succeed (Toplevel.no_timing o IsarCmd.class_deps));
 
 val _ =
   OuterSyntax.improper_command "thm_deps" "visualize theorem dependencies"
     K.diag (SpecParse.xthms1 >> (Toplevel.no_timing oo IsarCmd.thm_deps));
-
-local
-
-val criterion =
-  P.reserved "name" |-- P.!!! (P.$$$ ":" |-- P.xname) >> FindTheorems.Name ||
-  P.reserved "intro" >> K FindTheorems.Intro ||
-  P.reserved "elim" >> K FindTheorems.Elim ||
-  P.reserved "dest" >> K FindTheorems.Dest ||
-  P.reserved "solves" >> K FindTheorems.Solves ||
-  P.reserved "simp" |-- P.!!! (P.$$$ ":" |-- P.term) >> FindTheorems.Simp ||
-  P.term >> FindTheorems.Pattern;
-
-val options =
-  Scan.optional
-    (P.$$$ "(" |--
-      P.!!! (Scan.option P.nat -- Scan.optional (P.reserved "with_dups" >> K false) true
-        --| P.$$$ ")")) (NONE, true);
-in
-
-val _ =
-  OuterSyntax.improper_command "find_theorems" "print theorems meeting specified criteria" K.diag
-    (options -- Scan.repeat (((Scan.option P.minus >> is_none) -- criterion))
-      >> (Toplevel.no_timing oo IsarCmd.find_theorems));
-
-end;
-
-local
-
-val criterion =
-  P.reserved "strict" |-- P.!!! (P.$$$ ":" |-- P.xname) >> FindConsts.Strict ||
-  P.reserved "name" |-- P.!!! (P.$$$ ":" |-- P.xname) >> FindConsts.Name ||
-  P.xname >> FindConsts.Loose;
-
-in
-
-val _ =
-  OuterSyntax.improper_command "find_consts" "search constants by type pattern"
-    K.diag (Scan.repeat (((Scan.option P.minus >> is_none) -- criterion))
-            >> (Toplevel.no_timing oo IsarCmd.find_consts));
-
-end;
 
 val _ =
   OuterSyntax.improper_command "print_binds" "print term bindings of proof context" K.diag
     (Scan.succeed (Toplevel.no_timing o IsarCmd.print_binds));
 

     (Scan.option ((Scan.repeat1 (Scan.unless P.minus P.name) --| P.minus) --
        Scan.option (Scan.repeat1 (Scan.unless P.minus P.name))) >>
          (Toplevel.no_timing oo IsarCmd.unused_thms));
 
 
+
 (** system commands (for interactive mode only) **)
 
 val _ =
   OuterSyntax.improper_command "cd" "change current working directory" K.diag
     (P.path >> (Toplevel.no_timing oo IsarCmd.cd));

 
 val _ =
   OuterSyntax.improper_command "exit" "exit Isar loop" K.control
     (Scan.succeed (Toplevel.no_timing o IsarCmd.exit));
 
-val _ =
-  OuterSyntax.improper_command "welcome" "print welcome message" K.diag
-    (Scan.succeed (Toplevel.no_timing o IsarCmd.welcome));
-
 end;