2014-06-02 blanchet 2014-06-02 refactored Z3 to Isar proof construction code
2014-06-02 blanchet 2014-06-02 simplified counterexample handling
2014-06-02 blanchet 2014-06-02 split replay and proof parsing for Z3
2014-06-02 blanchet 2014-06-02 removed counterexample parser (obsolete and useless in practice)
2014-06-02 hoelzl 2014-06-02 remove superfluous assumption
2014-06-02 fleury 2014-06-02 basic setup for zipperposition prover
2014-06-02 desharna 2014-06-02 document property 'sel_set'
2014-06-02 desharna 2014-06-02 generate 'sel_set' theorem for (co)datatypes
2014-06-02 blanchet 2014-06-02 removed some spurious warnings in new (co)datatype package
2014-06-02 blanchet 2014-06-02 add option to keep duplicates, for more precise evaluation of relevance filters
2014-06-02 blanchet 2014-06-02 tuned whitespace
2014-06-01 haftmann 2014-06-01 definition in class: provide explicit auxiliary abbreviation carrying potential mixfix syntax in presence of dangling parameters
2014-06-01 haftmann 2014-06-01 tuned
2014-05-31 boehmes 2014-05-31 merged
2014-05-31 boehmes 2014-05-31 tuned
2014-05-31 boehmes 2014-05-31 more complete proof replay for Z3: support universally quantified rewrite steps
2014-05-31 haftmann 2014-05-31 postpone const declarations for nested context after canonical const declarations: keep const declarations stemming from interpretation together
2014-05-31 haftmann 2014-05-31 tuned
2014-05-31 haftmann 2014-05-31 explicit is better than implicit
2014-05-31 haftmann 2014-05-31 tuned names
2014-05-31 haftmann 2014-05-31 dropped accidental duplicate application of morphism
2014-05-30 hoelzl 2014-05-30 generalizd measurability on restricted space; rule for integrability on compact sets
2014-05-30 hoelzl 2014-05-30 better support for restrict_space
2014-05-30 nipkow 2014-05-30 must not cancel common factors on both sides of (in)equations in linear arithmetic decicision procedure
2014-05-30 wenzelm 2014-05-30 merged
2014-05-30 wenzelm 2014-05-30 updated cygwin -- include perl_vendor for libwww-perl;
2014-05-30 blanchet 2014-05-30 made 'Kuehlwein-style' be really like Python code, we now think
2014-05-30 blanchet 2014-05-30 make SML code closer to Python code when 'nb_kuehlwein_style' is true
2014-05-30 blanchet 2014-05-30 merge
2014-05-30 blanchet 2014-05-30 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
2014-05-30 hoelzl 2014-05-30 introduce more powerful reindexing rules for big operators
2014-05-30 wenzelm 2014-05-30 merged
2014-05-30 wenzelm 2014-05-30 make double-sure that old popup is dismissed, before replacing it;
2014-05-30 wenzelm 2014-05-30 more robust bold_style, e.g. relevant for accidental \<^bold> before keyword;
2014-05-30 blanchet 2014-05-30 added another way of invoking Python code, for experiments
2014-05-30 blanchet 2014-05-30 make SML naive Bayes closer to Python version
2014-05-30 blanchet 2014-05-30 tuned whitespace, to make datatype definitions slightly less intimidating
2014-05-30 blanchet 2014-05-30 more work on exporter
2014-05-30 blanchet 2014-05-30 got rid of 'linearize' option
2014-05-30 blanchet 2014-05-30 extend exporter with new versions of MaSh
2014-05-30 haftmann 2014-05-30 tuned
2014-05-30 haftmann 2014-05-30 tuned signature
2014-05-30 haftmann 2014-05-30 terminating code equations
2014-05-29 haftmann 2014-05-29 more direct passing of right-hand side
2014-05-29 haftmann 2014-05-29 even more uniform treatment of result after 95e5a633a18f
2014-05-29 paulson 2014-05-29 Merge
2014-05-29 paulson 2014-05-29 New theorems to enable the simplification of certain functions when applied to specific natural number constants (such as 4)
2014-05-29 nipkow 2014-05-29 removed Kleene_Algebra because of superior AFP entry; authors agreed
2014-05-29 nipkow 2014-05-29 typo
2014-05-28 haftmann 2014-05-28 uniform treatmen of result
2014-05-28 haftmann 2014-05-28 tuned variable names
2014-05-28 blanchet 2014-05-28 more generous max number of suggestions, for more safety
2014-05-28 blanchet 2014-05-28 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)
2014-05-28 blanchet 2014-05-28 export more ML functions, for experimentation
2014-05-28 wenzelm 2014-05-28 tuned signature;
2014-05-28 blanchet 2014-05-28 disabled IDF for now -- empirical evidence points the wrong way (as usual)
2014-05-28 blanchet 2014-05-28 tuning
2014-05-28 blanchet 2014-05-28 tuning
2014-05-28 blanchet 2014-05-28 optimized computation
2014-05-28 blanchet 2014-05-28 enabled IDF for naive Bayes ML