2010-11-04 haftmann 2010-11-04 corrected quoting
2010-11-04 haftmann 2010-11-04 added lemma length_alloc
2010-11-04 haftmann 2010-11-04 dropped return abbreviation for Pair -- confusing if combined with monad syntax; tuned document
2010-11-04 haftmann 2010-11-04 added note on countable types
2010-11-04 boehmes 2010-11-04 simulate more closely the behaviour of the tactic
2010-11-04 wenzelm 2010-11-04 merged
2010-11-04 haftmann 2010-11-04 merged
2010-11-04 haftmann 2010-11-04 merged
2010-11-03 haftmann 2010-11-03 dropped debug message
2010-11-03 haftmann 2010-11-03 more precise text
2010-11-03 haftmann 2010-11-03 SMLdummy target
2010-11-03 haftmann 2010-11-03 fixed typos
2010-11-03 haftmann 2010-11-03 moved theory Quicksort from Library/ to ex/
2010-11-03 haftmann 2010-11-03 Theory Multiset provides stable quicksort implementation of sort_key.
2010-11-03 haftmann 2010-11-03 added code lemmas for stable parametrized quicksort
2010-11-03 haftmann 2010-11-03 tuned proof
2010-11-04 blanchet 2010-11-04 moved file in makefile to reflect actual dependencies
2010-11-03 blanchet 2010-11-03 give E one more second, to prevent cases where it finds a proof but has no time to print it
2010-11-03 blanchet 2010-11-03 use floating-point numbers for Sledgehammer's "thresholds" option rather than percentages; updated docs
2010-11-03 blanchet 2010-11-03 don't be overly verbose in Sledgehammer's minimizer
2010-11-03 blanchet 2010-11-03 standardize on seconds for Nitpick and Sledgehammer timeouts
2010-11-03 nipkow 2010-11-03 cleaned up
2010-11-04 wenzelm 2010-11-04 added property "tooltip-margin";
2010-11-04 wenzelm 2010-11-04 clarified tooltips: message output by default, extra info via control/command;
2010-11-04 wenzelm 2010-11-04 warn in correlation with report -- avoid spurious message duplicates;
2010-11-04 wenzelm 2010-11-04 tuned;
2010-11-03 wenzelm 2010-11-03 feeder: treat header as escaped utf8 to allow initial ML text to refer to non-ASCII file/directory names (e.g. "Documents/" on Chinese Ubuntu);
2010-11-03 boehmes 2010-11-03 merged
2010-11-03 boehmes 2010-11-03 updated SMT certificates
2010-11-03 boehmes 2010-11-03 standardize timeout value based on reals
2010-11-03 wenzelm 2010-11-03 merged
2010-11-03 huffman 2010-11-03 merged
2010-10-30 huffman 2010-10-30 change default_sort of HOLCF from pcpo to bifinite; rename command 'new_domain' to 'domain'; rename 'domain' to 'domain (unsafe)'
2010-10-30 huffman 2010-10-30 merged
2010-10-29 huffman 2010-10-29 renamed {Rep,Abs}_CFun to {Rep,Abs}_cfun
2010-10-29 huffman 2010-10-29 renamed lemma cont2cont_Rep_CFun to cont2cont_APP
2010-10-29 huffman 2010-10-29 simplify proof of typedef_cont_Abs
2010-10-27 huffman 2010-10-27 rename constant trifte to tr_case
2010-10-27 huffman 2010-10-27 add 'LAM (Def x). t' as alternative syntax for 'FLIFT x. t'
2010-10-27 huffman 2010-10-27 make syntax of continuous if-then-else consistent with HOL if-then-else
2010-10-27 huffman 2010-10-27 rename lemmas *_defined_iff and *_strict_iff to *_bottom_iff
2010-11-03 haftmann 2010-11-03 polyml_as_definition does not require explicit dependencies on external ML files
2010-11-03 wenzelm 2010-11-03 explicit warning about opaque signature matching -- saves extra paragraph in implementation manual;
2010-11-03 wenzelm 2010-11-03 discontinued obsolete function sys_error and exception SYS_ERROR;
2010-11-03 wenzelm 2010-11-03 replaced ancient sys_error by raise Fail, assuming that the latter is not handled specifically by the environment;
2010-11-03 wenzelm 2010-11-03 replaced ancient sys_error by raise Fail, assuming that the latter is not handled specifically by the environment;
2010-11-03 wenzelm 2010-11-03 try_param_tac: plain user error appears more appropriate;
2010-11-03 wenzelm 2010-11-03 replaced ancient sys_error by raise Fail, assuming that the latter is not handled specifically by the environment;
2010-11-03 wenzelm 2010-11-03 eliminated dead code;
2010-11-03 wenzelm 2010-11-03 more conventional exceptions for abstract syntax operations -- eliminated ancient SYS_ERROR; proper signature constraint;
2010-11-03 nipkow 2010-11-03 removed assumption
2010-11-02 wenzelm 2010-11-02 more on naming tactics;
2010-11-02 wenzelm 2010-11-02 merged
2010-11-02 haftmann 2010-11-02 merged
2010-11-02 haftmann 2010-11-02 tuned proof
2010-11-02 haftmann 2010-11-02 tuned proof
2010-11-02 haftmann 2010-11-02 tuned lemma proposition of properties_for_sort_key
2010-11-02 haftmann 2010-11-02 lemmas sorted_map_same, sorted_same
2010-11-02 haftmann 2010-11-02 lemmas multiset_of_filter, sort_key_by_quicksort
2010-11-02 wenzelm 2010-11-02 more on "Time" in Isabelle/ML;