2012-06-05 haftmann 2012-06-05 prefer records with speaking labels over deeply nested tuples
2012-06-04 Andreas Lochbihler 2012-06-04 merged
2012-06-04 Andreas Lochbihler 2012-06-04 more sort constraints for FinFun code generation
2012-06-04 boehmes 2012-06-04 restricted Z3 by default to a fragment where proof reconstruction should not fail (for better integration with Sledgehammer) -- the full set of supported Z3 features can still be used by enabling the configuration option "z3_with_extensions"
2012-06-03 haftmann 2012-06-03 explicit check for correct number of arguments for abstract constructor
2012-06-02 huffman 2012-06-02 merged
2012-06-02 huffman 2012-06-02 transfer method now handles transfer rules for compound terms, e.g. locale-defined constants with hidden parameters
2012-06-01 huffman 2012-06-01 transfer method now avoids generalizing over free variables that are known to appear in registered transfer rules
2012-06-01 huffman 2012-06-01 unify theory-data structures for transfer package
2012-06-01 huffman 2012-06-01 remove duplicate lemma card_unit in favor of Finite_Set.card_UNIV_unit
2012-06-01 Andreas Lochbihler 2012-06-01 improved code setup for card, finite, subset
2012-06-01 Andreas Lochbihler 2012-06-01 merged
2012-06-01 Andreas Lochbihler 2012-06-01 more instantiations for card_UNIV, more lemmas for CARD
2012-06-01 Andreas Lochbihler 2012-06-01 simplify card_UNIV type class, tuned proofs
2012-06-01 Andreas Lochbihler 2012-06-01 drop redundant sort constraint
2012-06-01 wenzelm 2012-06-01 use \tocentry as in implementation manual;
2012-06-01 wenzelm 2012-06-01 tuned message;
2012-06-01 wenzelm 2012-06-01 tuned header;
2012-06-01 Andreas Lochbihler 2012-06-01 merged
2012-05-31 Andreas Lochbihler 2012-05-31 tuned proofs
2012-05-31 Andreas Lochbihler 2012-05-31 tuned instantiations dropped redundant lemmas
2012-05-31 Andreas Lochbihler 2012-05-31 unify Card_Univ and Cardinality
2012-05-31 huffman 2012-05-31 definition less_int_def has changed, use 'less_le' instead
2012-05-28 bulwahn 2012-05-28 adding incompleted simproc to rewrite set comprehensions into pointfree expressions on sets
2012-05-31 huffman 2012-05-31 remove stray reference to no-longer-existing theorem 'add'
2012-05-31 huffman 2012-05-31 temporarily comment out portion of Quotient_Examples/Quotient_Rat.thy, broken by changes to Int.thy
2012-05-30 huffman 2012-05-30 temporarily comment out nitpick examples broken by changes to Int.thy
2012-05-30 huffman 2012-05-30 convert Int.thy to use lifting and transfer
2012-05-30 huffman 2012-05-30 remove unnecessary simp rules involving Abs_Integ
2012-05-30 boehmes 2012-05-30 introduced option "z3_with_extensions" to control whether Z3's support for nonlinear arithmetic and datatypes should be enabled (including potential proof reconstruction failures)
2012-05-30 Andreas Lochbihler 2012-05-30 merged
2012-05-30 Andreas Lochbihler 2012-05-30 remove pretty syntax for FinFuns at the end and provide separate syntax theory
2012-05-29 huffman 2012-05-29 add lemma set_of_image_mset
2012-05-30 Andreas Lochbihler 2012-05-30 merged
2012-05-30 Andreas Lochbihler 2012-05-30 eliminated remaining sub- and superscripts in FinFun syntax
2012-05-30 Andreas Lochbihler 2012-05-30 syntax for FinFun composition without subscripts tuned proofs
2012-05-30 Andreas Lochbihler 2012-05-30 FinFun pseudo-constructor syntax without superscripts
2012-05-30 Andreas Lochbihler 2012-05-30 replace FinFun application syntax with $
2012-05-30 Andreas Lochbihler 2012-05-30 removed subscripts from FinFun type syntax
2012-05-30 Andreas Lochbihler 2012-05-30 improve code setup for set equality
2012-05-29 Andreas Lochbihler 2012-05-29 add code equation for coset xs = set ys
2012-05-29 Andreas Lochbihler 2012-05-29 tuned proofs
2012-05-29 Andreas Lochbihler 2012-05-29 use bundle in FinFun
2012-05-29 Andreas Lochbihler 2012-05-29 unify Rep_finfun and finfun_apply
2012-05-29 Andreas Lochbihler 2012-05-29 move FinFuns from AFP to repository
2012-05-30 wenzelm 2012-05-30 discontinued unused unzip/untar;
2012-05-29 wenzelm 2012-05-29 update GUI components after init;
2012-05-29 wenzelm 2012-05-29 merged
2012-05-29 kuncar 2012-05-29 don't be so aggressive during unfolding id and o
2012-05-29 huffman 2012-05-29 reordered sections
2012-05-29 wenzelm 2012-05-29 tuned message;
2012-05-29 wenzelm 2012-05-29 separate syslog dockable -- discontinued tendency of sub-window management via tabs;
2012-05-29 wenzelm 2012-05-29 clarified prover startup: no timeout, read stderr more carefully;
2012-05-29 wenzelm 2012-05-29 need to close_input before expecting threads to terminate/join; tuned signature;
2012-05-29 wenzelm 2012-05-29 make double sure that GUI components are up-to-date after init;
2012-05-29 wenzelm 2012-05-29 tuned message;
2012-05-29 wenzelm 2012-05-29 more explicit treatment of return code vs. session phase;
2012-05-29 wenzelm 2012-05-29 tuned signature;
2012-05-29 wenzelm 2012-05-29 separate README dockable, which allows to make it more prominent first and remove it later;
2012-05-29 bulwahn 2012-05-29 added optimisation for equational premises in Quickcheck; added some Quickcheck examples; NEWS