#
cea7d9ed |
|
25-Oct-2019 |
blanchet <none@none> |
compile
|
#
b97e6dae |
|
25-Oct-2019 |
blanchet <none@none> |
removed E-SInE, a very old system by now (and SInE has been incorporated in many provers in the past decade)
|
#
e60cf64d |
|
06-Jan-2019 |
wenzelm <none@none> |
isabelle update -u path_cartouches;
|
#
2dc6f8f0 |
|
11-Jul-2016 |
wenzelm <none@none> |
tuned;
|
#
1901affb |
|
18-Jul-2015 |
wenzelm <none@none> |
isabelle update_cartouches;
|
#
3c4cd10c |
|
29-Jan-2015 |
wenzelm <none@none> |
more explicit indication of Async_Manager_Legacy as Proof General legacy; --HG-- rename : src/HOL/Tools/Sledgehammer/async_manager.ML => src/HOL/Tools/Sledgehammer/async_manager_legacy.ML
|
#
794edf80 |
|
02-Nov-2014 |
wenzelm <none@none> |
modernized header uniformly as section;
|
#
ef3b9997 |
|
29-Sep-2014 |
blanchet <none@none> |
made 'moura' tactic more powerful
|
#
85d53264 |
|
28-Aug-2014 |
blanchet <none@none> |
moved skolem method
|
#
13c70a63 |
|
28-Aug-2014 |
blanchet <none@none> |
added 'skolem' method, esp. for 'obtain's generated from Z3 proofs
|
#
ac75f5e7 |
|
27-Aug-2014 |
blanchet <none@none> |
renamed new SMT module from 'SMT2' to 'SMT' --HG-- rename : src/HOL/SMT2.thy => src/HOL/SMT.thy rename : src/HOL/Tools/SMT2/smt2_builtin.ML => src/HOL/Tools/SMT/smt_builtin.ML rename : src/HOL/Tools/SMT2/smt2_config.ML => src/HOL/Tools/SMT/smt_config.ML rename : src/HOL/Tools/SMT2/smt2_datatypes.ML => src/HOL/Tools/SMT/smt_datatypes.ML rename : src/HOL/Tools/SMT2/smt2_failure.ML => src/HOL/Tools/SMT/smt_failure.ML rename : src/HOL/Tools/SMT2/smt2_normalize.ML => src/HOL/Tools/SMT/smt_normalize.ML rename : src/HOL/Tools/SMT2/smt2_real.ML => src/HOL/Tools/SMT/smt_real.ML rename : src/HOL/Tools/SMT2/smt2_solver.ML => src/HOL/Tools/SMT/smt_solver.ML rename : src/HOL/Tools/SMT2/smt2_systems.ML => src/HOL/Tools/SMT/smt_systems.ML rename : src/HOL/Tools/SMT2/smt2_translate.ML => src/HOL/Tools/SMT/smt_translate.ML rename : src/HOL/Tools/SMT2/smt2_util.ML => src/HOL/Tools/SMT/smt_util.ML rename : src/HOL/Tools/SMT2/smtlib2.ML => src/HOL/Tools/SMT/smtlib.ML rename : src/HOL/Tools/SMT2/smtlib2_interface.ML => src/HOL/Tools/SMT/smtlib_interface.ML rename : src/HOL/Tools/SMT2/smtlib2_isar.ML => src/HOL/Tools/SMT/smtlib_isar.ML rename : src/HOL/Tools/SMT2/smtlib2_proof.ML => src/HOL/Tools/SMT/smtlib_proof.ML rename : src/HOL/Tools/SMT2/verit_isar.ML => src/HOL/Tools/SMT/verit_isar.ML rename : src/HOL/Tools/SMT2/verit_proof.ML => src/HOL/Tools/SMT/verit_proof.ML rename : src/HOL/Tools/SMT2/verit_proof_parse.ML => src/HOL/Tools/SMT/verit_proof_parse.ML rename : src/HOL/Tools/SMT2/z3_new_interface.ML => src/HOL/Tools/SMT/z3_interface.ML rename : src/HOL/Tools/SMT2/z3_new_isar.ML => src/HOL/Tools/SMT/z3_isar.ML rename : src/HOL/Tools/SMT2/z3_new_proof.ML => src/HOL/Tools/SMT/z3_proof.ML rename : src/HOL/Tools/SMT2/z3_new_real.ML => src/HOL/Tools/SMT/z3_real.ML rename : src/HOL/Tools/SMT2/z3_new_replay.ML => src/HOL/Tools/SMT/z3_replay.ML rename : src/HOL/Tools/SMT2/z3_new_replay_literals.ML => src/HOL/Tools/SMT/z3_replay_literals.ML rename : src/HOL/Tools/SMT2/z3_new_replay_methods.ML => src/HOL/Tools/SMT/z3_replay_methods.ML rename : src/HOL/Tools/SMT2/z3_new_replay_rules.ML => src/HOL/Tools/SMT/z3_replay_rules.ML rename : src/HOL/Tools/SMT2/z3_new_replay_util.ML => src/HOL/Tools/SMT/z3_replay_util.ML rename : src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt2.ML => src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt.ML rename : src/HOL/Word/Tools/smt2_word.ML => src/HOL/Word/Tools/smt_word.ML
|
#
8e49e927 |
|
16-Jun-2014 |
blanchet <none@none> |
fixed parsing of one-argument 'file()' in TSTP files
|
#
122e0295 |
|
16-Jun-2014 |
blanchet <none@none> |
use right delimiters for Waldmeister proofs
|
#
dd2a0d80 |
|
16-Jun-2014 |
blanchet <none@none> |
simplified code
|
#
07041a99 |
|
16-Jun-2014 |
blanchet <none@none> |
moved code around --HG-- rename : src/HOL/Tools/Sledgehammer/sledgehammer_prover_waldmeister.ML => src/HOL/Tools/ATP/atp_waldmeister.ML
|
#
2fde10a4 |
|
12-Jun-2014 |
blanchet <none@none> |
tuned dependencies
|
#
d4fd6e53 |
|
11-Jun-2014 |
blanchet <none@none> |
reduces Sledgehammer dependencies
|
#
dc8e9ca7 |
|
11-Jun-2014 |
blanchet <none@none> |
moved new highly experimental Waldmeister-specific code (authored by Albert Steckermeier) into Isabelle
|
#
0b5e2e90 |
|
11-Jun-2014 |
blanchet <none@none> |
removed old SMT module from Sledgehammer
|
#
bf8eef3e |
|
14-Mar-2014 |
blanchet <none@none> |
undo rewrite rules (e.g. for 'fun_app') in Isar
|
#
00ff94c2 |
|
14-Mar-2014 |
blanchet <none@none> |
more simplification of trivial steps
|
#
f936bab5 |
|
13-Mar-2014 |
blanchet <none@none> |
integrate SMT2 with Sledgehammer
|
#
6b4f08d8 |
|
13-Mar-2014 |
blanchet <none@none> |
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
|
#
f0dd587a |
|
03-Feb-2014 |
blanchet <none@none> |
got rid of 'try0' step that is now redundant
|
#
700f2e9d |
|
03-Feb-2014 |
blanchet <none@none> |
renamed ML file --HG-- rename : src/HOL/Tools/Sledgehammer/sledgehammer_reconstructor.ML => src/HOL/Tools/Sledgehammer/sledgehammer_proof_methods.ML
|
#
945bedcb |
|
31-Jan-2014 |
blanchet <none@none> |
moved ML code around
|
#
06f3d979 |
|
30-Jan-2014 |
blanchet <none@none> |
refactor large ML file
|
#
eb52da60 |
|
31-Jan-2014 |
blanchet <none@none> |
renamed many Sledgehammer ML files to clarify structure --HG-- rename : src/HOL/Tools/Sledgehammer/sledgehammer_run.ML => src/HOL/Tools/Sledgehammer/sledgehammer.ML rename : src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML => src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML rename : src/HOL/Tools/Sledgehammer/sledgehammer_annotate.ML => src/HOL/Tools/Sledgehammer/sledgehammer_isar_annotate.ML rename : src/HOL/Tools/Sledgehammer/sledgehammer_compress.ML => src/HOL/Tools/Sledgehammer/sledgehammer_isar_compress.ML rename : src/HOL/Tools/Sledgehammer/sledgehammer_minimize_isar.ML => src/HOL/Tools/Sledgehammer/sledgehammer_isar_minimize.ML rename : src/HOL/Tools/Sledgehammer/sledgehammer_preplay.ML => src/HOL/Tools/Sledgehammer/sledgehammer_isar_preplay.ML rename : src/HOL/Tools/Sledgehammer/sledgehammer_print.ML => src/HOL/Tools/Sledgehammer/sledgehammer_isar_print.ML rename : src/HOL/Tools/Sledgehammer/sledgehammer_proof.ML => src/HOL/Tools/Sledgehammer/sledgehammer_isar_proof.ML rename : src/HOL/Tools/Sledgehammer/sledgehammer_try0.ML => src/HOL/Tools/Sledgehammer/sledgehammer_isar_try0.ML rename : src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML => src/HOL/Tools/Sledgehammer/sledgehammer_prover_minimize.ML
|
#
b58b6956 |
|
31-Jan-2014 |
blanchet <none@none> |
renamed ML file --HG-- rename : src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML => src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML
|
#
7c06c38c |
|
31-Jan-2014 |
blanchet <none@none> |
tuned ML file name --HG-- rename : src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML => src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML
|
#
215faebc |
|
20-Dec-2013 |
blanchet <none@none> |
reconstruct SPASS-Pirate steps of the form 'x ~= C x' (or more complicated)
|
#
68670fb3 |
|
12-Jul-2013 |
wenzelm <none@none> |
hybrid "auto" tool setup, for TTY (within theory) and PIDE (global print function);
|
#
fde18fe4 |
|
12-Jul-2013 |
smolkas <none@none> |
minimize dependencies (used facts) of Isar proof steps; remove unreferenced steps
|
#
54afc8fd |
|
11-Jul-2013 |
smolkas <none@none> |
optimize isar-proofs by trying different proof methods
|
#
b5cb9c44 |
|
09-Jul-2013 |
smolkas <none@none> |
moved code -> easier debugging
|
#
b28fd8f3 |
|
17-Feb-2013 |
smolkas <none@none> |
split isar_step into isar_step, fix, assms; made isar_proof explicit; register fixed variables in ctxt and auto_fix terms to avoid superfluous annotations
|
#
e1a92caa |
|
17-Feb-2013 |
smolkas <none@none> |
simplified byline, isar_qualifier
|
#
583ed312 |
|
14-Feb-2013 |
smolkas <none@none> |
renamed sledgehammer_shrink to sledgehammer_compress --HG-- rename : src/HOL/Tools/Sledgehammer/sledgehammer_shrink.ML => src/HOL/Tools/Sledgehammer/sledgehammer_compress.ML
|
#
2b1e6fd8 |
|
17-Jan-2013 |
smolkas <none@none> |
move preplaying to own structure
|
#
b0c749ce |
|
27-Nov-2012 |
smolkas <none@none> |
renamed sledgehammer_isar_reconstruct to sledgehammer_proof --HG-- rename : src/HOL/Tools/Sledgehammer/sledgehammer_isar_Reconstruct.ML => src/HOL/Tools/Sledgehammer/sledgehammer_proof.ML
|
#
2aba4bb9 |
|
27-Nov-2012 |
smolkas <none@none> |
put shrink in own structure
|
#
2af79422 |
|
27-Nov-2012 |
smolkas <none@none> |
put annotate in own structure
|
#
ad099505 |
|
16-Oct-2012 |
blanchet <none@none> |
added proof minimization code from Steffen Smolka
|
#
e3227796 |
|
22-Aug-2012 |
wenzelm <none@none> |
prefer ML_file over old uses;
|
#
b2844097 |
|
20-Jul-2012 |
blanchet <none@none> |
renamed ML files --HG-- rename : src/HOL/Tools/Sledgehammer/sledgehammer_filter_mash.ML => src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML rename : src/HOL/Tools/Sledgehammer/sledgehammer_filter_iter.ML => src/HOL/Tools/Sledgehammer/sledgehammer_mepo.ML
|
#
f917ce87 |
|
18-Jul-2012 |
blanchet <none@none> |
rationalize relevance filter, slowing moving code from Iter to MaSh
|
#
6e993fb8 |
|
11-Jul-2012 |
blanchet <none@none> |
moved most of MaSh exporter code to Sledgehammer
|
#
a74b00cb |
|
11-Jul-2012 |
blanchet <none@none> |
further ML structure split to permit finer-grained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
|
#
870593bf |
|
15-Mar-2012 |
wenzelm <none@none> |
declare command keywords via theory header, including strict checking outside Pure;
|
#
47a925bb |
|
31-May-2011 |
blanchet <none@none> |
first step in sharing more code between ATP and Metis translation --HG-- rename : src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML => src/HOL/Tools/ATP/atp_reconstruct.ML rename : src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML => src/HOL/Tools/ATP/atp_translate.ML
|
#
247df2ed |
|
02-May-2011 |
wenzelm <none@none> |
added Attrib.setup_config_XXX conveniences, with implicit setup of the background theory; proper name bindings;
|
#
bc2c0a1f |
|
09-Dec-2010 |
blanchet <none@none> |
compile
|
#
c7c67363 |
|
08-Dec-2010 |
blanchet <none@none> |
split "Sledgehammer" module into two parts, to resolve forthcoming dependency problems --HG-- rename : src/HOL/Tools/Sledgehammer/sledgehammer.ML => src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML rename : src/HOL/Tools/Sledgehammer/sledgehammer.ML => src/HOL/Tools/Sledgehammer/sledgehammer_run.ML
|
#
5580ed1a |
|
07-Dec-2010 |
blanchet <none@none> |
load "try" after "Metis" and move "Async_Manager" back to Sledgehammer --HG-- rename : src/HOL/Tools/async_manager.ML => src/HOL/Tools/Sledgehammer/async_manager.ML
|
#
beb1bdb2 |
|
26-Oct-2010 |
blanchet <none@none> |
integrated "smt" proof method with Sledgehammer
|
#
0891da48 |
|
25-Oct-2010 |
blanchet <none@none> |
reverted e7a80c6752c9 -- there's not much point in putting a diagnosis tool (as opposed to a proof method) in Plain, but more importantly Sledgehammer must be in Main to use SMT solvers
|
#
a9beedd9 |
|
25-Oct-2010 |
haftmann <none@none> |
moved sledgehammer to Plain; tuned dependencies
|
#
712c0bed |
|
22-Oct-2010 |
blanchet <none@none> |
renamed files --HG-- rename : src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML => src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML rename : src/HOL/Tools/Sledgehammer/sledgehammer_translate.ML => src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML
|
#
79078c7d |
|
05-Oct-2010 |
blanchet <none@none> |
factor out "ATP" from "Sledgehammer" (cf. "SAT" vs. "Refute", etc.) -- the theories now reflect the directory structure
|
#
e8c452f8 |
|
04-Oct-2010 |
blanchet <none@none> |
tuning
|
#
37d247fe |
|
04-Oct-2010 |
blanchet <none@none> |
move Metis into Plain --HG-- rename : src/HOL/Tools/Sledgehammer/metis_reconstruct.ML => src/HOL/Tools/Metis/metis_reconstruct.ML rename : src/HOL/Tools/Sledgehammer/metis_tactics.ML => src/HOL/Tools/Metis/metis_tactics.ML rename : src/HOL/Tools/Sledgehammer/metis_translate.ML => src/HOL/Tools/Metis/metis_translate.ML
|
#
d3bb2d81 |
|
04-Oct-2010 |
blanchet <none@none> |
remove Meson from Sledgehammer
|
#
caa0abe0 |
|
30-Sep-2010 |
blanchet <none@none> |
encode number of skolem assumptions in them, for more efficient retrieval later
|
#
c137d849 |
|
29-Sep-2010 |
blanchet <none@none> |
finished renaming file and module
|
#
ecd99500 |
|
29-Sep-2010 |
blanchet <none@none> |
rename file --HG-- rename : src/HOL/Tools/Sledgehammer/meson_clausifier.ML => src/HOL/Tools/Sledgehammer/meson_clausify.ML
|
#
b7577520 |
|
27-Sep-2010 |
blanchet <none@none> |
rename "Clausifier" to "Meson_Clausifier" and merge with "Meson_Tactic" --HG-- rename : src/HOL/Tools/Sledgehammer/clausifier.ML => src/HOL/Tools/Sledgehammer/meson_clausifier.ML
|
#
e1a68078 |
|
16-Sep-2010 |
blanchet <none@none> |
added new "Metis_Reconstruct" module, temporarily empty
|
#
d86baa55 |
|
16-Sep-2010 |
blanchet <none@none> |
rename "Metis_Clauses" to "Metis_Translate" for consistency with "Sledgehammer_Translate" --HG-- rename : src/HOL/Tools/Sledgehammer/metis_clauses.ML => src/HOL/Tools/Sledgehammer/metis_translate.ML
|
#
acf1190a |
|
16-Sep-2010 |
blanchet <none@none> |
factored out TSTP/SPASS/Vampire proof parsing; from "Sledgehammer_Reconstructo" to a new module "ATP_Proof"
|
#
1ffcc376 |
|
14-Sep-2010 |
blanchet <none@none> |
rename internal Sledgehammer constant
|
#
6e07a7c5 |
|
11-Sep-2010 |
blanchet <none@none> |
setup Auto Sledgehammer
|
#
2bc6dfb5 |
|
02-Sep-2010 |
blanchet <none@none> |
use definitional CNFs in Metis rather than plain CNF, following a suggestion by Joe Hurd; this *really* speeds up things -- HOL now builds 12% faster on my machine
|
#
c73a293d |
|
31-Aug-2010 |
blanchet <none@none> |
finish moving file
|
#
3c56c5f7 |
|
31-Aug-2010 |
blanchet <none@none> |
finished renaming
|
#
74ff17e4 |
|
19-Aug-2010 |
blanchet <none@none> |
encode "fequal" reasoning rules in Metis problem, just as is done for Sledgehammer -- otherwise any proof that relies on "fequal" found by Sledgehammer can't be reconstructed
|
#
9aaf659f |
|
08-Aug-2010 |
blanchet <none@none> |
move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML) --HG-- rename : src/HOL/Tools/Sledgehammer/sledgehammer_fact_minimizer.ML => src/HOL/Tools/Sledgehammer/sledgehammer_fact_minimize.ML
|
#
c88c7aa6 |
|
28-Jul-2010 |
blanchet <none@none> |
consequence of directory renaming
|
#
b308172d |
|
27-Jul-2010 |
blanchet <none@none> |
minor refactoring
|
#
de653e29 |
|
27-Jul-2010 |
blanchet <none@none> |
standardize "Author" tags
|
#
d643f8a9 |
|
27-Jul-2010 |
blanchet <none@none> |
reorder ML files in theory
|
#
50652674 |
|
27-Jul-2010 |
blanchet <none@none> |
more refactoring
|
#
fb6f46bb |
|
27-Jul-2010 |
blanchet <none@none> |
rename "ATP_Manager" ML module to "Sledgehammer"; more refactoring to come
|
#
fb393796 |
|
27-Jul-2010 |
blanchet <none@none> |
complete renaming of "Sledgehammer_TPTP_Format" to "ATP_Problem"
|
#
1278c0f0 |
|
28-Jun-2010 |
blanchet <none@none> |
no setup is necessary anymore
|
#
121f6fba |
|
25-Jun-2010 |
blanchet <none@none> |
factored non-ATP specific code from "ATP_Manager" out, so that it can be reused for the LEO-II integration
|
#
631c19fa |
|
25-Jun-2010 |
blanchet <none@none> |
reorder ML files
|
#
8fca933e |
|
25-Jun-2010 |
blanchet <none@none> |
renamed "Sledgehammer_FOL_Clauses" to "Metis_Clauses", so that Metis doesn't depend on Sledgehammer --HG-- rename : src/HOL/Tools/Sledgehammer/sledgehammer_fol_clause.ML => src/HOL/Tools/Sledgehammer/metis_clauses.ML
|
#
056d9ac6 |
|
25-Jun-2010 |
blanchet <none@none> |
merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
|
#
28ffd341 |
|
25-Jun-2010 |
blanchet <none@none> |
renamed "Sledgehammer_Fact_Preprocessor" to "Clausifier"; the new name reflects that it's not used only by Sledgehammer (but also by "meson" and "metis") and that it doesn't only clausify facts (but also goals) --HG-- rename : src/HOL/Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML => src/HOL/Tools/Sledgehammer/clausifier.ML
|
#
c0584048 |
|
25-Jun-2010 |
blanchet <none@none> |
more moving around of ML files in "Sledgehammer.thy"
|
#
5f5351d8 |
|
25-Jun-2010 |
blanchet <none@none> |
move "MESON" up; the ultimate goal is to make Sledgehammer depend on MESON and Metis, rather than a big spaghetti
|
#
c82e78b8 |
|
24-Jun-2010 |
blanchet <none@none> |
never include anything from the Sledgehammer theory in the relevant facts + killed two obsolete facts
|
#
831a6abc |
|
23-Jun-2010 |
blanchet <none@none> |
killed legacy "neg_clausify" and "clausify"
|
#
d5610740 |
|
22-Jun-2010 |
blanchet <none@none> |
factor out TPTP format output into file of its own, to facilitate further changes
|
#
66878b3f |
|
14-Jun-2010 |
blanchet <none@none> |
adjusted the polymorphism handling of Skolem constants so that proof reconstruction doesn't fail in "equality_inf"
|
#
eb75e9ae |
|
11-Jun-2010 |
blanchet <none@none> |
proper polymorphic Skolemization of uncached facts + synchronization of caching and relevance filter
|
#
5aea423c |
|
30-Apr-2010 |
blanchet <none@none> |
added "no_atp" for theorems that are automatically used or included by Sledgehammer when appropriate (about combinators and fequal)
|
#
23f7b381 |
|
25-Apr-2010 |
blanchet <none@none> |
move "neg_clausify" method and "clausify" attribute to "sledgehammer_isar.ML"
|
#
0dee4905 |
|
23-Apr-2010 |
blanchet <none@none> |
now rename the file "atp_wrapper.ML" to "atp_systems.ML" + fix typo in "SystemOnTPTP" script --HG-- rename : src/HOL/Tools/ATP_Manager/atp_wrapper.ML => src/HOL/Tools/ATP_Manager/atp_systems.ML
|
#
c63aa835 |
|
23-Apr-2010 |
blanchet <none@none> |
renamed module "ATP_Wrapper" to "ATP_Systems"
|
#
057278ac |
|
23-Apr-2010 |
blanchet <none@none> |
move the minimizer to the Sledgehammer directory --HG-- rename : src/HOL/Tools/ATP_Manager/atp_minimal.ML => src/HOL/Tools/Sledgehammer/sledgehammer_fact_minimizer.ML
|
#
a5f9c697 |
|
29-Mar-2010 |
blanchet <none@none> |
added "modulus" and "sorts" options to control Sledgehammer's Isar proof output
|
#
3afc9c82 |
|
29-Mar-2010 |
blanchet <none@none> |
get rid of Polyhash, since it's no longer used
|
#
6149474e |
|
23-Mar-2010 |
blanchet <none@none> |
add new file "sledgehammer_util.ML" to setup
|
#
f0f4208a |
|
19-Mar-2010 |
blanchet <none@none> |
move all ATP setup code into ATP_Wrapper
|
#
538e54e9 |
|
19-Mar-2010 |
blanchet <none@none> |
move the Sledgehammer Isar commands together into one file; this will make easier to add options and reorganize them later
|
#
e9669e5e |
|
19-Mar-2010 |
blanchet <none@none> |
more Sledgehammer refactoring
|
#
eaf6f9f8 |
|
17-Mar-2010 |
blanchet <none@none> |
renamed "ATP_Linkup" theory to "Sledgehammer" --HG-- rename : src/HOL/ATP_Linkup.thy => src/HOL/Sledgehammer.thy
|