src/HOL/Tools/ATP_Manager/atp_manager.ML
changeset 35866 513074557e06
parent 35865 2f8fb5242799
child 35867 16279c4c7a33
     1.1 --- a/src/HOL/Tools/ATP_Manager/atp_manager.ML	Fri Mar 19 13:02:18 2010 +0100
     1.2 +++ b/src/HOL/Tools/ATP_Manager/atp_manager.ML	Fri Mar 19 15:07:44 2010 +0100
     1.3 @@ -282,36 +282,4 @@
     1.4      val _ = List.app (fn name => start_prover name birth_time death_time 1 proof_state) provers;
     1.5    in () end;
     1.6  
     1.7 -
     1.8 -
     1.9 -(** Isar command syntax **)
    1.10 -
    1.11 -local structure K = OuterKeyword and P = OuterParse in
    1.12 -
    1.13 -val _ =
    1.14 -  OuterSyntax.improper_command "atp_kill" "kill all managed provers" K.diag
    1.15 -    (Scan.succeed (Toplevel.no_timing o Toplevel.imperative kill));
    1.16 -
    1.17 -val _ =
    1.18 -  OuterSyntax.improper_command "atp_info" "print information about managed provers" K.diag
    1.19 -    (Scan.succeed (Toplevel.no_timing o Toplevel.imperative info));
    1.20 -
    1.21 -val _ =
    1.22 -  OuterSyntax.improper_command "atp_messages" "print recent messages issued by managed provers" K.diag
    1.23 -    (Scan.option (P.$$$ "(" |-- P.nat --| P.$$$ ")") >>
    1.24 -      (fn limit => Toplevel.no_timing o Toplevel.imperative (fn () => messages limit)));
    1.25 -
    1.26 -val _ =
    1.27 -  OuterSyntax.improper_command "print_atps" "print external provers" K.diag
    1.28 -    (Scan.succeed (Toplevel.no_timing o Toplevel.unknown_theory o
    1.29 -      Toplevel.keep (print_provers o Toplevel.theory_of)));
    1.30 -
    1.31 -val _ =
    1.32 -  OuterSyntax.command "sledgehammer" "call all automatic theorem provers" K.diag
    1.33 -    (Scan.repeat P.xname >> (fn names => Toplevel.no_timing o Toplevel.unknown_proof o
    1.34 -      Toplevel.keep (sledgehammer names o Toplevel.proof_of)));
    1.35 -
    1.36  end;
    1.37 -
    1.38 -end;
    1.39 -