Tue, 03 Jun 2014 16:22:01 +0200 hoelzl use 0 as integral-value for non-integrable functions, simplify a couple of rewrite rules
Tue, 03 Jun 2014 11:43:07 +0200 blanchet removed SMT weights -- their impact was very inconclusive anyway
Tue, 03 Jun 2014 10:35:51 +0200 blanchet make SMT code less dependent on Z3 proofs
Tue, 03 Jun 2014 10:13:44 +0200 blanchet tuning
Mon, 02 Jun 2014 22:38:46 +0200 blanchet avoid division by 0
Mon, 02 Jun 2014 19:21:41 +0200 haftmann formal treatment of dangling parameters for class abbrevs analogously to class consts
Mon, 02 Jun 2014 19:21:40 +0200 haftmann explicit passing of params
Mon, 02 Jun 2014 17:34:27 +0200 blanchet refactored Z3 to Isar proof construction code
Mon, 02 Jun 2014 17:34:26 +0200 blanchet simplified counterexample handling
Mon, 02 Jun 2014 17:34:26 +0200 blanchet split replay and proof parsing for Z3
Mon, 02 Jun 2014 17:34:25 +0200 blanchet removed counterexample parser (obsolete and useless in practice)
Mon, 02 Jun 2014 16:19:37 +0200 hoelzl remove superfluous assumption
Mon, 02 Jun 2014 15:10:18 +0200 fleury basic setup for zipperposition prover
Mon, 02 Jun 2014 14:29:20 +0200 desharna document property 'sel_set'
Mon, 02 Jun 2014 14:29:20 +0200 desharna generate 'sel_set' theorem for (co)datatypes
Mon, 02 Jun 2014 11:59:51 +0200 blanchet removed some spurious warnings in new (co)datatype package
Mon, 02 Jun 2014 11:59:50 +0200 blanchet add option to keep duplicates, for more precise evaluation of relevance filters
Mon, 02 Jun 2014 11:59:49 +0200 blanchet tuned whitespace
Sun, 01 Jun 2014 14:00:58 +0200 haftmann definition in class: provide explicit auxiliary abbreviation carrying potential mixfix syntax in presence of dangling parameters
Sun, 01 Jun 2014 08:33:35 +0200 haftmann tuned
Sat, 31 May 2014 23:00:13 +0200 boehmes merged
Sat, 31 May 2014 22:59:54 +0200 boehmes tuned
Sat, 31 May 2014 22:31:03 +0200 boehmes more complete proof replay for Z3: support universally quantified rewrite steps
Sat, 31 May 2014 09:35:12 +0200 haftmann postpone const declarations for nested context after canonical const declarations: keep const declarations stemming from interpretation together
Sat, 31 May 2014 09:35:10 +0200 haftmann tuned
Sat, 31 May 2014 09:35:09 +0200 haftmann explicit is better than implicit
Sat, 31 May 2014 09:35:08 +0200 haftmann tuned names
Sat, 31 May 2014 09:35:07 +0200 haftmann dropped accidental duplicate application of morphism
Fri, 30 May 2014 18:48:05 +0200 hoelzl generalizd measurability on restricted space; rule for integrability on compact sets
Fri, 30 May 2014 15:56:30 +0200 hoelzl better support for restrict_space
Fri, 30 May 2014 18:13:40 +0200 nipkow must not cancel common factors on both sides of (in)equations in linear arithmetic decicision procedure
Fri, 30 May 2014 16:10:57 +0200 wenzelm merged
Fri, 30 May 2014 15:34:14 +0200 wenzelm updated cygwin -- include perl_vendor for libwww-perl;
Fri, 30 May 2014 16:00:54 +0200 blanchet made 'Kuehlwein-style' be really like Python code, we now think
Fri, 30 May 2014 15:15:41 +0200 blanchet make SML code closer to Python code when 'nb_kuehlwein_style' is true
Fri, 30 May 2014 15:15:02 +0200 blanchet merge
Fri, 30 May 2014 14:43:06 +0200 blanchet added sleep to give time for the server to shut down -- this is a hack, but it's only in experimental code that will hopefully soon go away
Fri, 30 May 2014 14:55:10 +0200 hoelzl introduce more powerful reindexing rules for big operators
Fri, 30 May 2014 12:54:42 +0200 wenzelm merged
Fri, 30 May 2014 11:02:02 +0200 wenzelm make double-sure that old popup is dismissed, before replacing it;
Fri, 30 May 2014 10:50:57 +0200 wenzelm more robust bold_style, e.g. relevant for accidental \<^bold> before keyword;
Fri, 30 May 2014 12:27:51 +0200 blanchet added another way of invoking Python code, for experiments
Fri, 30 May 2014 12:27:51 +0200 blanchet make SML naive Bayes closer to Python version
Fri, 30 May 2014 12:27:51 +0200 blanchet tuned whitespace, to make datatype definitions slightly less intimidating
Fri, 30 May 2014 12:27:51 +0200 blanchet more work on exporter
Fri, 30 May 2014 12:27:51 +0200 blanchet got rid of 'linearize' option
Fri, 30 May 2014 12:27:51 +0200 blanchet extend exporter with new versions of MaSh
Fri, 30 May 2014 08:23:08 +0200 haftmann tuned
Fri, 30 May 2014 08:23:07 +0200 haftmann tuned signature
Fri, 30 May 2014 08:23:07 +0200 haftmann terminating code equations
Thu, 29 May 2014 22:46:21 +0200 haftmann more direct passing of right-hand side
Thu, 29 May 2014 22:46:20 +0200 haftmann even more uniform treatment of result after 95e5a633a18f
Thu, 29 May 2014 15:27:49 +0100 paulson Merge
Thu, 29 May 2014 14:39:19 +0100 paulson New theorems to enable the simplification of certain functions when applied to specific natural number constants (such as 4)
Thu, 29 May 2014 16:13:47 +0200 nipkow removed Kleene_Algebra because of superior AFP entry; authors agreed
Thu, 29 May 2014 11:11:22 +0200 nipkow typo
Wed, 28 May 2014 19:18:18 +0200 haftmann uniform treatmen of result
Wed, 28 May 2014 19:17:32 +0200 haftmann tuned variable names
Wed, 28 May 2014 17:42:36 +0200 blanchet more generous max number of suggestions, for more safety
Wed, 28 May 2014 17:42:34 +0200 blanchet changed MaSh to use SML version instead of Python version of naive Bayes by default (i.e. if MASH=yes in the settings, or 'fact_filter=mash' with no other explicit setting)
(0) -30000 -10000 -3000 -1000 -300 -100 -60 +60 +100 +300 +1000 +3000 +10000 tip