equal
deleted
inserted
replaced
7 header {* Sledgehammer: Isabelle--ATP Linkup *} |
7 header {* Sledgehammer: Isabelle--ATP Linkup *} |
8 |
8 |
9 theory Sledgehammer |
9 theory Sledgehammer |
10 imports ATP SMT |
10 imports ATP SMT |
11 keywords "sledgehammer" :: diag and "sledgehammer_params" :: thy_decl |
11 keywords "sledgehammer" :: diag and "sledgehammer_params" :: thy_decl |
12 uses "Tools/Sledgehammer/async_manager.ML" |
|
13 "Tools/Sledgehammer/sledgehammer_util.ML" |
|
14 "Tools/Sledgehammer/sledgehammer_fact.ML" |
|
15 "Tools/Sledgehammer/sledgehammer_provers.ML" |
|
16 "Tools/Sledgehammer/sledgehammer_minimize.ML" |
|
17 "Tools/Sledgehammer/sledgehammer_mepo.ML" |
|
18 "Tools/Sledgehammer/sledgehammer_mash.ML" |
|
19 "Tools/Sledgehammer/sledgehammer_run.ML" |
|
20 "Tools/Sledgehammer/sledgehammer_isar.ML" |
|
21 begin |
12 begin |
|
13 |
|
14 ML_file "Tools/Sledgehammer/async_manager.ML" |
|
15 ML_file "Tools/Sledgehammer/sledgehammer_util.ML" |
|
16 ML_file "Tools/Sledgehammer/sledgehammer_fact.ML" |
|
17 ML_file "Tools/Sledgehammer/sledgehammer_provers.ML" |
|
18 ML_file "Tools/Sledgehammer/sledgehammer_minimize.ML" |
|
19 ML_file "Tools/Sledgehammer/sledgehammer_mepo.ML" |
|
20 ML_file "Tools/Sledgehammer/sledgehammer_mash.ML" |
|
21 ML_file "Tools/Sledgehammer/sledgehammer_run.ML" |
|
22 ML_file "Tools/Sledgehammer/sledgehammer_isar.ML" |
22 |
23 |
23 setup {* Sledgehammer_Isar.setup *} |
24 setup {* Sledgehammer_Isar.setup *} |
24 |
25 |
25 end |
26 end |