wenzelm [Sat, 27 Mar 2010 16:01:45 +0100] rev 35987
disallow sort constraints in primitive Theory.add_axiom/add_def -- handled in Thm.add_axiom/add_def;
wenzelm [Sat, 27 Mar 2010 15:47:57 +0100] rev 35986
added Term.fold_atyps_sorts convenience;
wenzelm [Sat, 27 Mar 2010 15:20:31 +0100] rev 35985
moved Drule.forall_intr_frees to Thm.forall_intr_frees (in more_thm.ML, which is loaded before pure_thy.ML);
discontinued old-style Theory.add_defs(_i) in favour of more basic Theory.add_def;
modernized PureThy.add_defs etc. -- refer to high-level Thm.add_def;
wenzelm [Sat, 27 Mar 2010 14:10:37 +0100] rev 35984
eliminated old-style Theory.add_defs_i;
boehmes [Sat, 27 Mar 2010 02:10:00 +0100] rev 35983
slightly more general simproc (avoids errors of linarith)
boehmes [Sat, 27 Mar 2010 00:08:39 +0100] rev 35982
merged
boehmes [Fri, 26 Mar 2010 23:58:27 +0100] rev 35981
updated SMT certificates
boehmes [Fri, 26 Mar 2010 23:57:35 +0100] rev 35980
made renamings stable under name changes in the original problem (uninterpreted names are irrelevant to the SMT solver, and caching of SMT certificates relies on irrelevancy of renamings)
boehmes [Fri, 26 Mar 2010 23:46:22 +0100] rev 35979
replaced references 'trace_simp' and 'debug_simp' by configuration options stored in the context
wenzelm [Fri, 26 Mar 2010 20:30:03 +0100] rev 35978
merged
hoelzl [Fri, 26 Mar 2010 18:03:01 +0100] rev 35977
Added finite measure space.
wenzelm [Fri, 26 Mar 2010 20:30:05 +0100] rev 35976
tuned white space;
wenzelm [Fri, 26 Mar 2010 20:28:15 +0100] rev 35975
more efficient merge_algebra for important special cases -- tricky due to required completion if class algebra changes;
wenzelm [Fri, 26 Mar 2010 17:59:11 +0100] rev 35974
low-level tuning for join/merge: ignore identical versions (SUBTLE CHANGE IN SEMANTICS);
wenzelm [Thu, 25 Mar 2010 23:18:42 +0100] rev 35973
merged
blanchet [Thu, 25 Mar 2010 17:56:31 +0100] rev 35972
merged
blanchet [Thu, 25 Mar 2010 17:55:55 +0100] rev 35971
make Mirabelle happy again
blanchet [Wed, 24 Mar 2010 14:51:36 +0100] rev 35970
revert debugging output that shouldn't have been submitted in the first place
blanchet [Wed, 24 Mar 2010 14:49:32 +0100] rev 35969
added support for Sledgehammer parameters;
this change goes hand in hand with f8c738abaed8
blanchet [Wed, 24 Mar 2010 14:43:35 +0100] rev 35968
simplify Nitpick parameter parsing code a little bit + make compile
blanchet [Wed, 24 Mar 2010 12:31:37 +0100] rev 35967
add new file "sledgehammer_util.ML" to setup
blanchet [Wed, 24 Mar 2010 12:30:33 +0100] rev 35966
honor the newly introduced Sledgehammer parameters and fixed the parsing;
e.g. the prover "e_isar" (formely "e_full") is gone, instead do sledgehammer [atps = e, isar_proof] to get the same effect
blanchet [Tue, 23 Mar 2010 14:43:22 +0100] rev 35965
added a syntax for specifying facts to Sledgehammer;
e.g., sledgehammer (add: foo del: bar)
which tells the relevance filter to include "foo" but omit "bar".
blanchet [Tue, 23 Mar 2010 11:40:46 +0100] rev 35964
leverage code now in Sledgehammer
blanchet [Tue, 23 Mar 2010 11:39:21 +0100] rev 35963
added options to Sledgehammer;
syntax: sledgehammer [options] goal_no, where "[options]" and "goal_no" are optional
blanchet [Mon, 22 Mar 2010 15:23:18 +0100] rev 35962
make "sledgehammer" and "atp_minimize" improper commands
wenzelm [Thu, 25 Mar 2010 21:27:04 +0100] rev 35961
Sorts.of_sort_derivation: do not use slow Graph.irreducible_paths here, which not always needed (SUBTLE CHANGE IN SEMANTICS);
officially export weaken as Sorts.classrel_derivation;
tuned comments;
wenzelm [Thu, 25 Mar 2010 21:14:15 +0100] rev 35960
removed unused AxClass.of_sort derivation;