Fri, 21 Nov 2014 12:11:44 +0100 Andreas Lochbihler register pmf as BNF
Thu, 20 Nov 2014 17:29:18 +0100 blanchet added CVC4 option that helps on JD
Thu, 20 Nov 2014 17:29:18 +0100 blanchet always generate patterns as lists of lists, to avoid confusing CVC4 (and stick to what SMT-LIB 2 actually says)
Thu, 20 Nov 2014 17:29:18 +0100 blanchet work around bug in CVC4, with boolean arguments to (co)datatypes
Thu, 20 Nov 2014 17:29:18 +0100 blanchet other way of crashing (with CVC4)
Thu, 20 Nov 2014 17:29:18 +0100 blanchet set right logic for CVC4 with (co)datatypes
Thu, 20 Nov 2014 17:29:18 +0100 blanchet removed explicit '--quant-cf' option to CVC4, now that it's the default
Wed, 19 Nov 2014 19:12:14 +0100 traytel more accurate lemma name
Wed, 19 Nov 2014 10:31:15 +0100 blanchet parse CVC4 unsat cores
Wed, 19 Nov 2014 10:31:15 +0100 blanchet tuning
Wed, 19 Nov 2014 10:31:15 +0100 blanchet removed redundant code line
Tue, 18 Nov 2014 20:56:34 +0100 wenzelm clarified Table.make_set: duplicate arguments are allowed, like Table.make_list or Scala Set() formation;
Mon, 17 Nov 2014 18:19:06 +0100 hoelzl add reindex rules for distr and nn_integral on count_space
Mon, 17 Nov 2014 14:55:34 +0100 haftmann generalized lemmas and tuned proofs
Mon, 17 Nov 2014 14:55:33 +0100 haftmann generalized lemmas (particularly concerning dvd) as far as appropriate
Mon, 17 Nov 2014 14:55:32 +0100 haftmann formally self-contained gcd type classes
Fri, 14 Nov 2014 22:13:45 +0100 wenzelm merged
Fri, 14 Nov 2014 21:36:50 +0100 wenzelm no quick_and_dirty for proof extraction, to avoid obscure errors like "corr: bad proof";
Fri, 14 Nov 2014 17:07:06 +0100 wenzelm use \isastyletext directly via 'text' command;
Fri, 14 Nov 2014 11:19:14 +0100 wenzelm proper sequential version (cf. 302104d8366b);
Fri, 14 Nov 2014 18:39:42 +0100 haftmann documentation stubs about permanent_interpretation
Fri, 14 Nov 2014 13:18:33 +0100 hoelzl cleaning up some theorem names; remove unnecessary assumptions; more complete pmf theory
Fri, 14 Nov 2014 08:18:58 +0100 hoelzl merged
Thu, 13 Nov 2014 17:19:52 +0100 hoelzl import general theorems from AFP/Markov_Models
Thu, 13 Nov 2014 23:45:15 +0100 wenzelm uniform treatment of all document markup commands: 'text' and 'txt' merely differ in LaTeX style;
Thu, 13 Nov 2014 17:28:11 +0100 blanchet tuning
Thu, 13 Nov 2014 14:40:06 +0100 traytel merged
Thu, 13 Nov 2014 14:14:13 +0100 traytel do not introduce consts too early unnecessarily
Thu, 13 Nov 2014 12:35:55 +0100 nipkow added lemma
Wed, 12 Nov 2014 19:30:56 +0100 wenzelm merged
Wed, 12 Nov 2014 18:18:38 +0100 wenzelm prefer independent parallel map where user input is processed -- avoid non-deterministic feedback in error situations;
Wed, 12 Nov 2014 11:39:27 +0100 wenzelm make SML/NJ happy;
Wed, 12 Nov 2014 10:30:59 +0100 wenzelm more careful ML source positions, for improved PIDE markup;
Wed, 12 Nov 2014 17:37:44 +0100 immler NEWS
Wed, 12 Nov 2014 17:37:43 +0100 immler tuned proofs
Wed, 12 Nov 2014 17:37:43 +0100 immler added quickcheck[approximation]
Wed, 12 Nov 2014 17:37:43 +0100 immler quickcheck setup for float, inspired by rat::{exhaustive,full_exhaustive,random}
Wed, 12 Nov 2014 17:37:43 +0100 immler disjunction and conjunction for forms
Wed, 12 Nov 2014 17:37:43 +0100 immler truncate intermediate results in horner to improve performance of approximate;
Wed, 12 Nov 2014 17:36:36 +0100 immler added lemmas: convert between powr and log in comparisons, pull log out of addition/subtraction
Wed, 12 Nov 2014 17:36:32 +0100 immler cancel real of power of numeral also for equality and strict inequality;
Wed, 12 Nov 2014 17:36:29 +0100 immler simplified computations based on round_up by reducing to round_down;
Wed, 12 Nov 2014 17:36:25 +0100 immler code equation for powr
Tue, 11 Nov 2014 21:14:19 +0100 wenzelm merged
Tue, 11 Nov 2014 20:11:38 +0100 wenzelm more careful ML source positions, for improved PIDE markup;
Tue, 11 Nov 2014 18:16:25 +0100 wenzelm more position information, e.g. relevant for errors in generated ML source;
Tue, 11 Nov 2014 15:55:31 +0100 wenzelm more symbols;
Tue, 11 Nov 2014 13:50:56 +0100 wenzelm tuned whitespace;
Tue, 11 Nov 2014 13:44:09 +0100 wenzelm more markup;
Tue, 11 Nov 2014 13:40:13 +0100 wenzelm simplifie sessions;
Tue, 11 Nov 2014 11:47:53 +0100 wenzelm more Isar proof methods;
Tue, 11 Nov 2014 11:41:58 +0100 wenzelm more Isar proof methods;
Tue, 11 Nov 2014 10:54:52 +0100 wenzelm more Isar proof methods;
Tue, 11 Nov 2014 19:38:45 +0100 noschinl add forgotten lemma
Tue, 11 Nov 2014 14:46:26 +0100 noschinl added lemma
Tue, 11 Nov 2014 12:30:37 +0100 desharna make 'corec_transfer' tactic more robust
Tue, 11 Nov 2014 12:30:36 +0100 desharna also generate '(co)rec_transfer' for (co)datatypes with 0 live type variables
Tue, 11 Nov 2014 10:26:08 +0100 desharna make 'rec_transfer' tactic more robust
Tue, 11 Nov 2014 08:57:46 +0100 Andreas Lochbihler add del option to measurable;
Tue, 11 Nov 2014 00:11:11 +0100 wenzelm merged
(0) -30000 -10000 -3000 -1000 -300 -100 -60 +60 +100 +300 +1000 +3000 +10000 tip