Wed, 23 Jun 2010 10:20:33 +0200 |
blanchet |
this looks like the most appropriate place to do the beta-eta-contraction
|
file |
diff |
annotate
|
Wed, 23 Jun 2010 09:40:06 +0200 |
blanchet |
killed legacy "neg_clausify" and "clausify"
|
file |
diff |
annotate
|
Tue, 22 Jun 2010 16:23:29 +0200 |
blanchet |
thread original theorem along with CNF theorem, as a step toward killing the Skolem cache
|
file |
diff |
annotate
|
Tue, 22 Jun 2010 14:28:22 +0200 |
blanchet |
removed Sledgehammer's support for the DFG syntax;
|
file |
diff |
annotate
|
Tue, 22 Jun 2010 13:17:17 +0200 |
blanchet |
reintroduce new Sledgehammer polymorphic handling code;
|
file |
diff |
annotate
|
Tue, 22 Jun 2010 01:21:52 +0200 |
blanchet |
reredisable new polymorphic code
|
file |
diff |
annotate
|
Mon, 21 Jun 2010 18:32:16 +0200 |
blanchet |
beta-eta was too much, because it transformed SOME x. P x into Eps P, which caused problems later;
|
file |
diff |
annotate
|
Tue, 15 Jun 2010 16:42:09 +0200 |
blanchet |
found missing beta-eta-contraction
|
file |
diff |
annotate
|
Mon, 14 Jun 2010 21:49:25 +0200 |
blanchet |
turn off new polymorphism code again -- a new issue popped up
|
file |
diff |
annotate
|
Mon, 14 Jun 2010 19:20:32 +0200 |
blanchet |
no point in introducing combinators for inlined Skolem functions
|
file |
diff |
annotate
|
Mon, 14 Jun 2010 10:36:01 +0200 |
blanchet |
adjusted the polymorphism handling of Skolem constants so that proof reconstruction doesn't fail in "equality_inf"
|
file |
diff |
annotate
|
Sat, 12 Jun 2010 11:12:31 +0200 |
blanchet |
disable new polymorphic code for now, until remaining issues in "equality_inf" are resolved
|
file |
diff |
annotate
|
Fri, 11 Jun 2010 17:10:23 +0200 |
blanchet |
proper polymorphic Skolemization of uncached facts + synchronization of caching and relevance filter
|
file |
diff |
annotate
|
Mon, 07 Jun 2010 10:37:06 +0200 |
blanchet |
cosmetics
|
file |
diff |
annotate
|
Sat, 05 Jun 2010 21:30:40 +0200 |
blanchet |
renaming
|
file |
diff |
annotate
|
Sat, 05 Jun 2010 16:39:23 +0200 |
blanchet |
show more respect for user-specified facts, even if they could lead to unsound proofs + don't throw away "unsound" theorems in "full_type" mode, since they are then sound
|
file |
diff |
annotate
|
Sat, 05 Jun 2010 15:59:58 +0200 |
blanchet |
make Sledgehammer's "add:" and "del:" syntax work better in the presence of aliases;
|
file |
diff |
annotate
|
Fri, 04 Jun 2010 16:55:08 +0200 |
blanchet |
don't raise Option.Option if assumptions contain schematic variables
|
file |
diff |
annotate
|
Fri, 28 May 2010 13:49:21 +0200 |
blanchet |
make sure chained facts appear in Isar proofs generated by Sledgehammer -- otherwise the proof won't work
|
file |
diff |
annotate
|
Sat, 15 May 2010 21:50:05 +0200 |
wenzelm |
less pervasive names from structure Thm;
|
file |
diff |
annotate
|
Fri, 30 Apr 2010 23:53:37 +0200 |
wenzelm |
renamed Variable.thm_context to Variable.global_thm_context to emphasize that this is not the real thing;
|
file |
diff |
annotate
|
Wed, 28 Apr 2010 15:53:17 +0200 |
blanchet |
save the name of Skolemized variables in Sledgehammer for use in the proof reconstruction code
|
file |
diff |
annotate
|
Tue, 27 Apr 2010 16:00:20 +0200 |
blanchet |
fix types of "fix" variables to help proof reconstruction and aid readability
|
file |
diff |
annotate
|
Mon, 26 Apr 2010 21:16:35 +0200 |
blanchet |
make "neg_clausify" return a list of lists of clauses, so that it's possible to see which clause comes from which theorem
|
file |
diff |
annotate
|
Sun, 25 Apr 2010 14:40:36 +0200 |
blanchet |
move "neg_clausify" method and "clausify" attribute to "sledgehammer_isar.ML"
|
file |
diff |
annotate
|
Sun, 25 Apr 2010 11:38:46 +0200 |
blanchet |
support readable names even when Isar proof reconstruction is enabled -- useful for debugging
|
file |
diff |
annotate
|
Mon, 19 Apr 2010 16:33:48 +0200 |
blanchet |
got rid of somewhat pointless "pairname" function in Sledgehammer
|
file |
diff |
annotate
|
Sun, 11 Apr 2010 14:30:34 +0200 |
wenzelm |
Thm.add_axiom/add_def: return internal name of foundational axiom;
|
file |
diff |
annotate
|
Sat, 27 Mar 2010 14:10:37 +0100 |
wenzelm |
eliminated old-style Theory.add_defs_i;
|
file |
diff |
annotate
|
Thu, 25 Mar 2010 17:55:55 +0100 |
blanchet |
make Mirabelle happy again
|
file |
diff |
annotate
|
Tue, 23 Mar 2010 11:39:21 +0100 |
blanchet |
added options to Sledgehammer;
|
file |
diff |
annotate
|
Mon, 22 Mar 2010 10:25:44 +0100 |
blanchet |
merged
|
file |
diff |
annotate
|
Mon, 22 Mar 2010 10:25:07 +0100 |
blanchet |
start work on direct proof reconstruction for Sledgehammer
|
file |
diff |
annotate
|
Fri, 19 Mar 2010 13:02:18 +0100 |
blanchet |
more Sledgehammer refactoring
|
file |
diff |
annotate
|
Sat, 20 Mar 2010 17:33:11 +0100 |
wenzelm |
renamed varify/unvarify operations to varify_global/unvarify_global to emphasize that these only work in a global situation;
|
file |
diff |
annotate
|
Thu, 18 Mar 2010 12:58:52 +0100 |
blanchet |
now use "Named_Thms" for "noatp", and renamed "noatp" to "no_atp"
|
file |
diff |
annotate
|
Wed, 17 Mar 2010 19:26:05 +0100 |
blanchet |
renamed Sledgehammer structures
|
file |
diff |
annotate
|
Wed, 17 Mar 2010 18:16:31 +0100 |
blanchet |
move Sledgehammer files in a directory of their own
|
file |
diff |
annotate
| base
|