| author | wenzelm |
| Fri Mar 07 22:30:58 2014 +0100 (2014-03-07) | |
| changeset 55990 | 41c6b99c5fb7 |
| parent 55287 | ffa306239316 |
| child 56078 | 624faeda77b5 |
| permissions | -rw-r--r-- |
| blanchet@35827 | 1 |
(* Title: HOL/Sledgehammer.thy |
| blanchet@38027 | 2 |
Author: Lawrence C. Paulson, Cambridge University Computer Laboratory |
| blanchet@38028 | 3 |
Author: Jia Meng, Cambridge University Computer Laboratory and NICTA |
| blanchet@35865 | 4 |
Author: Jasmin Blanchette, TU Muenchen |
| wenzelm@21254 | 5 |
*) |
| wenzelm@21254 | 6 |
|
| blanchet@35827 | 7 |
header {* Sledgehammer: Isabelle--ATP Linkup *}
|
| wenzelm@21254 | 8 |
|
| blanchet@35827 | 9 |
theory Sledgehammer |
| blanchet@40181 | 10 |
imports ATP SMT |
| wenzelm@46950 | 11 |
keywords "sledgehammer" :: diag and "sledgehammer_params" :: thy_decl |
| wenzelm@21254 | 12 |
begin |
| wenzelm@21254 | 13 |
|
| blanchet@54838 | 14 |
lemma size_ne_size_imp_ne: "size x \<noteq> size y \<Longrightarrow> x \<noteq> y" |
| blanchet@54838 | 15 |
by (erule contrapos_nn) (rule arg_cong) |
| blanchet@54838 | 16 |
|
| wenzelm@48891 | 17 |
ML_file "Tools/Sledgehammer/async_manager.ML" |
| wenzelm@48891 | 18 |
ML_file "Tools/Sledgehammer/sledgehammer_util.ML" |
| wenzelm@48891 | 19 |
ML_file "Tools/Sledgehammer/sledgehammer_fact.ML" |
| blanchet@55287 | 20 |
ML_file "Tools/Sledgehammer/sledgehammer_proof_methods.ML" |
| blanchet@55211 | 21 |
ML_file "Tools/Sledgehammer/sledgehammer_isar_annotate.ML" |
| blanchet@55202 | 22 |
ML_file "Tools/Sledgehammer/sledgehammer_isar_proof.ML" |
| blanchet@55202 | 23 |
ML_file "Tools/Sledgehammer/sledgehammer_isar_preplay.ML" |
| blanchet@55202 | 24 |
ML_file "Tools/Sledgehammer/sledgehammer_isar_compress.ML" |
| blanchet@55202 | 25 |
ML_file "Tools/Sledgehammer/sledgehammer_isar_minimize.ML" |
| blanchet@55202 | 26 |
ML_file "Tools/Sledgehammer/sledgehammer_isar.ML" |
| blanchet@55201 | 27 |
ML_file "Tools/Sledgehammer/sledgehammer_prover.ML" |
| blanchet@55205 | 28 |
ML_file "Tools/Sledgehammer/sledgehammer_prover_atp.ML" |
| blanchet@55205 | 29 |
ML_file "Tools/Sledgehammer/sledgehammer_prover_smt.ML" |
| blanchet@55202 | 30 |
ML_file "Tools/Sledgehammer/sledgehammer_prover_minimize.ML" |
| wenzelm@48891 | 31 |
ML_file "Tools/Sledgehammer/sledgehammer_mepo.ML" |
| wenzelm@48891 | 32 |
ML_file "Tools/Sledgehammer/sledgehammer_mash.ML" |
| blanchet@55202 | 33 |
ML_file "Tools/Sledgehammer/sledgehammer.ML" |
| blanchet@55198 | 34 |
ML_file "Tools/Sledgehammer/sledgehammer_commands.ML" |
| wenzelm@48891 | 35 |
|
| wenzelm@21254 | 36 |
end |