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
paulson <lp15@cam.ac.uk> [Wed, 29 Jan 2014 15:41:18 +0000] rev 55162
Merge
paulson <lp15@cam.ac.uk> [Wed, 29 Jan 2014 15:40:33 +0000] rev 55161
minor adjustments
blanchet [Wed, 29 Jan 2014 15:05:53 +0100] rev 55160
added Dmitriy, since he did the case syntax
paulson <lp15@cam.ac.uk> [Wed, 29 Jan 2014 12:51:37 +0000] rev 55159
Replacing the theory Library/Binomial by Number_Theory/Binomial
paulson <lp15@cam.ac.uk> [Mon, 27 Jan 2014 17:13:33 +0000] rev 55158
Merge