blanchet [Mon, 03 Feb 2014 13:37:23 +0100] rev 55282
tuning
blanchet [Mon, 03 Feb 2014 13:35:50 +0100] rev 55281
refactor relabeling code
blanchet [Mon, 03 Feb 2014 11:58:38 +0100] rev 55280
tuned data structure
blanchet [Mon, 03 Feb 2014 11:37:48 +0100] rev 55279
tuned data structure
blanchet [Mon, 03 Feb 2014 11:30:53 +0100] rev 55278
more flexible compression, choosing whichever proof method works
blanchet [Mon, 03 Feb 2014 10:19:19 +0100] rev 55277
reduced preplaying timeout, since (1) Isar proofs are getting better and better as alternatives; (2) the same timeout is used for each step in an Isar proof, where a lower timeout makes more sense
blanchet [Mon, 03 Feb 2014 10:14:18 +0100] rev 55276
made SML/NJ happier
blanchet [Mon, 03 Feb 2014 10:14:18 +0100] rev 55275
less aggressive evaluation
blanchet [Mon, 03 Feb 2014 10:14:18 +0100] rev 55274
added a new version of 'metis' to the mix
blanchet [Mon, 03 Feb 2014 10:14:18 +0100] rev 55273
implemented new 'try0_isar' semantics
blanchet [Mon, 03 Feb 2014 10:14:18 +0100] rev 55272
tuning
blanchet [Mon, 03 Feb 2014 10:14:18 +0100] rev 55271
better time slack, to account for ultra-quick proof methods
blanchet [Mon, 03 Feb 2014 10:14:18 +0100] rev 55270
crucial fix: use right version of the step
blanchet [Mon, 03 Feb 2014 10:14:18 +0100] rev 55269
more thorough, hybrid compression
blanchet [Mon, 03 Feb 2014 10:14:18 +0100] rev 55268
tuning
blanchet [Mon, 03 Feb 2014 10:14:18 +0100] rev 55267
got rid of 'try0' step that is now redundant
blanchet [Mon, 03 Feb 2014 10:14:18 +0100] rev 55266
centralize more preplaying
blanchet [Mon, 03 Feb 2014 10:14:18 +0100] rev 55265
tuning
blanchet [Mon, 03 Feb 2014 10:14:18 +0100] rev 55264
centralize preplaying
blanchet [Mon, 03 Feb 2014 10:14:18 +0100] rev 55263
tuned
paulson <lp15@cam.ac.uk> [Mon, 03 Feb 2014 00:22:48 +0000] rev 55262
fixed indentation
paulson <lp15@cam.ac.uk> [Sun, 02 Feb 2014 21:48:28 +0000] rev 55261
new lemmas involving phi from Lehmer AFP entry
blanchet [Sun, 02 Feb 2014 20:53:51 +0100] rev 55260
more data structure rationalization
blanchet [Sun, 02 Feb 2014 20:53:51 +0100] rev 55259
tuning
blanchet [Sun, 02 Feb 2014 20:53:51 +0100] rev 55258
more data structure rationalization
blanchet [Sun, 02 Feb 2014 20:53:51 +0100] rev 55257
rationalized threading of 'metis' arguments
blanchet [Sun, 02 Feb 2014 20:53:51 +0100] rev 55256
refactored data structure (step 3)
blanchet [Sun, 02 Feb 2014 20:53:51 +0100] rev 55255
refactoring of data structure (step 2)
blanchet [Sun, 02 Feb 2014 20:53:51 +0100] rev 55254
'primitive' is not an adverb
blanchet [Sun, 02 Feb 2014 20:53:51 +0100] rev 55253
unform treatment of preplay_timeout = 0 and > 0
blanchet [Sun, 02 Feb 2014 20:53:51 +0100] rev 55252
refactor data structure (step 1)
blanchet [Sun, 02 Feb 2014 20:53:51 +0100] rev 55251
tuned code
blanchet [Sun, 02 Feb 2014 20:53:51 +0100] rev 55250
tuned factor
blanchet [Sun, 02 Feb 2014 20:53:51 +0100] rev 55249
tuning
blanchet [Sun, 02 Feb 2014 20:53:51 +0100] rev 55248
made SML/NJ happier
blanchet [Sun, 02 Feb 2014 20:53:51 +0100] rev 55247
take intersection rather than union of methods when merging steps -- more efficient and natural
blanchet [Sun, 02 Feb 2014 20:53:51 +0100] rev 55246
merge proof methods
blanchet [Sun, 02 Feb 2014 20:53:51 +0100] rev 55245
use Skolem proof methods appropriately
blanchet [Sun, 02 Feb 2014 20:53:51 +0100] rev 55244
simplified data structure -- eliminated distinction between 'first-class' and 'second-class' proof methods
blanchet [Sun, 02 Feb 2014 20:53:51 +0100] rev 55243
reset timing information after changes
paulson <lp15@cam.ac.uk> [Sun, 02 Feb 2014 19:15:25 +0000] rev 55242
Number_Theory: prime is no longer overloaded, but only for nat. Automatic coercion to int enabled.
wenzelm [Sat, 01 Feb 2014 22:02:20 +0100] rev 55241
merged
wenzelm [Sat, 01 Feb 2014 21:43:23 +0100] rev 55240
proper config options;
proper context for printing;
wenzelm [Sat, 01 Feb 2014 21:09:53 +0100] rev 55239
more standard file/module names;
paulson <lp15@cam.ac.uk> [Sat, 01 Feb 2014 20:38:29 +0000] rev 55238
Added material from Old_Number_Theory related to the Chinese Remainder Theorem
wenzelm [Sat, 01 Feb 2014 20:46:19 +0100] rev 55237
prefer top-down rewriting for output (i.e. uncheck), in accordance to term abbreviations (see 5d2fe4e09354) and AST translations;
wenzelm [Sat, 01 Feb 2014 18:42:46 +0100] rev 55236
proper context for printing;
wenzelm [Sat, 01 Feb 2014 18:41:48 +0100] rev 55235
more explicit low-level exception;
wenzelm [Sat, 01 Feb 2014 18:40:47 +0100] rev 55234
unused;
wenzelm [Sat, 01 Feb 2014 18:22:38 +0100] rev 55233
method_setup "lem";
wenzelm [Sat, 01 Feb 2014 18:17:13 +0100] rev 55232
lazy_pack is default context for ILL;
wenzelm [Sat, 01 Feb 2014 18:07:10 +0100] rev 55231
unused;
wenzelm [Sat, 01 Feb 2014 18:05:03 +0100] rev 55230
proper Simplifier method setup;
wenzelm [Sat, 01 Feb 2014 18:00:28 +0100] rev 55229
simplified sessions;
wenzelm [Sat, 01 Feb 2014 17:56:03 +0100] rev 55228
misc tuning and modernization;
paulson <lp15@cam.ac.uk> [Sat, 01 Feb 2014 00:32:32 +0000] rev 55227
version of Fermat's Theorem for type nat
wenzelm [Fri, 31 Jan 2014 19:32:13 +0100] rev 55226
merged
wenzelm [Fri, 31 Jan 2014 18:58:50 +0100] rev 55225
merged
wenzelm [Fri, 31 Jan 2014 17:35:19 +0100] rev 55224
include comment.sty 3.6 which still works with plain tex, in contrast to later 3.7 which is only for latex (slow due to file snippets) -- see also 30781cc78fc6;
blanchet [Fri, 31 Jan 2014 19:16:41 +0100] rev 55223
generalized preplaying infrastructure to store various results for various methods
blanchet [Fri, 31 Jan 2014 18:43:16 +0100] rev 55222
added a 'trace' option
blanchet [Fri, 31 Jan 2014 18:43:16 +0100] rev 55221
tuning
blanchet [Fri, 31 Jan 2014 18:43:16 +0100] rev 55220
moved code around
blanchet [Fri, 31 Jan 2014 18:43:16 +0100] rev 55219
added 'algebra' to the mix
blanchet [Fri, 31 Jan 2014 18:43:16 +0100] rev 55218
more informative trace
blanchet [Fri, 31 Jan 2014 18:43:16 +0100] rev 55217
tuning
blanchet [Fri, 31 Jan 2014 18:43:16 +0100] rev 55216
more concise Isar output
paulson <lp15@cam.ac.uk> [Fri, 31 Jan 2014 16:58:58 +0000] rev 55215
Restoring some proofs from the equivalent file in Old_Number_Theory.
blanchet [Fri, 31 Jan 2014 16:41:54 +0100] rev 55214
better tracing + syntactically correct 'metis' calls
blanchet [Fri, 31 Jan 2014 16:26:43 +0100] rev 55213
tuned ML function names
blanchet [Fri, 31 Jan 2014 16:10:39 +0100] rev 55212
tuning
blanchet [Fri, 31 Jan 2014 16:07:20 +0100] rev 55211
moved ML code around
wenzelm [Fri, 31 Jan 2014 14:33:02 +0100] rev 55210
tuned headers;
blanchet [Fri, 31 Jan 2014 13:45:39 +0100] rev 55209
merge
blanchet [Fri, 31 Jan 2014 13:42:47 +0100] rev 55208
compile
blanchet [Fri, 31 Jan 2014 13:32:13 +0100] rev 55207
guarded against exception
blanchet [Fri, 31 Jan 2014 13:29:20 +0100] rev 55206
tuning
blanchet [Fri, 31 Jan 2014 12:30:54 +0100] rev 55205
refactor large ML file
traytel [Fri, 31 Jan 2014 12:16:59 +0100] rev 55204
use Local_Theory.define instead of Specification.definition for internal constants
blanchet [Fri, 31 Jan 2014 10:34:20 +0100] rev 55203
compile
blanchet [Fri, 31 Jan 2014 10:23:32 +0100] rev 55202
renamed many Sledgehammer ML files to clarify structure
blanchet [Fri, 31 Jan 2014 10:23:32 +0100] rev 55201
renamed ML file
blanchet [Fri, 31 Jan 2014 10:23:32 +0100] rev 55200
tuned comment
blanchet [Fri, 31 Jan 2014 10:23:32 +0100] rev 55199
tuned ML file name
blanchet [Fri, 31 Jan 2014 10:23:32 +0100] rev 55198
tuned ML file name
traytel [Fri, 31 Jan 2014 10:02:36 +0100] rev 55197
less hermetic tactics
blanchet [Thu, 30 Jan 2014 22:55:52 +0100] rev 55196
merged
blanchet [Thu, 30 Jan 2014 22:42:29 +0100] rev 55195
reverted unsound optimization
blanchet [Thu, 30 Jan 2014 21:56:25 +0100] rev 55194
got rid of one of two Metis variants
blanchet [Thu, 30 Jan 2014 21:02:19 +0100] rev 55193
tuning
blanchet [Thu, 30 Jan 2014 20:39:49 +0100] rev 55192
unskolemize SPASS formula to ensure that the variables are in the right order for 'metis's skolemizer
blanchet [Thu, 30 Jan 2014 18:37:08 +0100] rev 55191
killed needless pass
haftmann [Thu, 30 Jan 2014 16:30:01 +0100] rev 55190
dependency reporting for code generation errors
haftmann [Thu, 30 Jan 2014 16:30:00 +0100] rev 55189
more abstract dictionary construction
haftmann [Thu, 30 Jan 2014 16:09:04 +0100] rev 55188
reduced prominence of "permissive code generation"
haftmann [Thu, 30 Jan 2014 16:09:03 +0100] rev 55187
split rules for of_bool, similar to if
blanchet [Thu, 30 Jan 2014 17:34:42 +0100] rev 55186
don't forget the last inference(s) after conjecture skolemization
blanchet [Thu, 30 Jan 2014 16:40:31 +0100] rev 55185
centralized & repaired handling of bound variables in intermediate data structure (viva de Bruijn)
blanchet [Thu, 30 Jan 2014 15:01:40 +0100] rev 55184
keep formula right before skolemization, because the universal variables might be different (or differently ordered) as in the original axiom or negated conjecture from which it was skolemized
blanchet [Thu, 30 Jan 2014 14:37:53 +0100] rev 55183
renamed Sledgehammer options for symmetry between positive and negative versions
blanchet [Thu, 30 Jan 2014 14:28:04 +0100] rev 55182
more robust w.r.t. exceptions raised by proof methods
blanchet [Thu, 30 Jan 2014 14:24:10 +0100] rev 55181
tuning
blanchet [Thu, 30 Jan 2014 13:54:12 +0100] rev 55180
compile
blanchet [Thu, 30 Jan 2014 13:39:57 +0100] rev 55179
tuning
blanchet [Thu, 30 Jan 2014 13:38:28 +0100] rev 55178
added 'algebra' and 'meson' to 'try0'
blanchet [Thu, 30 Jan 2014 13:38:28 +0100] rev 55177
made 'try0' (more) silent
blanchet [Thu, 30 Jan 2014 13:38:28 +0100] rev 55176
'using' already uses the new Skolemizer, enabling a subtly shorter syntax
traytel [Thu, 30 Jan 2014 13:31:56 +0100] rev 55175
merged
traytel [Thu, 30 Jan 2014 12:28:05 +0100] rev 55174
extended cardinals library
traytel [Thu, 30 Jan 2014 12:27:42 +0100] rev 55173
define ofilter outside of wo_rel
haftmann [Thu, 30 Jan 2014 10:00:53 +0100] rev 55172
more direct simplification rules for 1 div/mod numeral;
added simplification rules for (- 1) div/mod numeral
blanchet [Thu, 30 Jan 2014 01:03:55 +0100] rev 55171
systematically suppress tracing if asked for (affects 'meson' proof method)
blanchet [Thu, 30 Jan 2014 00:59:12 +0100] rev 55170
silenced reconstructors in Sledgehammer
blanchet [Wed, 29 Jan 2014 23:24:34 +0100] rev 55169
proper 'show' detection
blanchet [Wed, 29 Jan 2014 22:34:34 +0100] rev 55168
correctly handle exceptions arising from (experimental) Isar proof code
haftmann [Wed, 29 Jan 2014 20:11:38 +0100] rev 55167
made smlnj happy
paulson <lp15@cam.ac.uk> [Wed, 29 Jan 2014 17:09:46 +0000] rev 55166
Merge
paulson <lp15@cam.ac.uk> [Wed, 29 Jan 2014 17:09:01 +0000] rev 55165
Removed a dependence upon Old_Number_Theory. Simplified a few proofs.
traytel [Wed, 29 Jan 2014 16:47:06 +0100] rev 55164
merged
traytel [Wed, 29 Jan 2014 16:35:05 +0100] rev 55163
made tactic more robust