2015-04-10 nipkow 2015-04-10 merged
2015-04-10 nipkow 2015-04-10 renamed Multiset.fold -> fold_mset, Multiset.filter -> filter_mset
2015-04-10 wenzelm 2015-04-10 tuned proofs;
2015-04-09 blanchet 2015-04-09 introduced new abbreviations for multiset operations (in the hope of getting rid of the old names <, <=, etc.)
2015-04-08 blanchet 2015-04-08 renamed multiset ordering to free up nice <# etc. symbols for the standard subset
2015-04-07 nipkow 2015-04-07 Removed mcard because it is equal to size
2015-03-23 haftmann 2015-03-23 explicit commutative additive inverse operation; more explicit focal point for commutative monoids with an inverse operation
2015-03-25 blanchet 2015-03-25 more multiset theorems
2015-03-25 wenzelm 2015-03-25 prefer local fixes;
2015-03-06 wenzelm 2015-03-06 proper context;
2015-02-19 haftmann 2015-02-19 establish unique preferred fact names
2014-11-02 wenzelm 2014-11-02 modernized header;
2014-09-24 blanchet 2014-09-24 simpler proof
2014-09-09 nipkow 2014-09-09 enamed drop_Suc_conv_tl and nth_drop' to Cons_nth_drop_Suc
2014-08-30 haftmann 2014-08-30 inlined unused definition
2014-08-22 blanchet 2014-08-22 added lemmas contributed by Rene Thiemann
2014-08-17 blanchet 2014-08-17 use 'image_mset' as BNF map function
2014-07-05 haftmann 2014-07-05 refrain from auxiliary abbreviation: be more explicit to the reader in situations where syntax translation does not apply; uniform appearance of xsymbol and HTML output for sums
2014-07-05 haftmann 2014-07-05 prefer ac_simps collections over separate name bindings for add and mult
2014-07-04 haftmann 2014-07-04 reduced name variants for assoc and commute on plus and mult
2014-06-11 Thomas Sewell 2014-06-11 Hypsubst preserves equality hypotheses Fixes included for various theories affected by this change.
2014-06-28 haftmann 2014-06-28 fact consolidation
2014-04-23 blanchet 2014-04-23 size function for multisets
2014-03-06 blanchet 2014-03-06 renamed 'fun_rel' to 'rel_fun'
2014-03-05 wenzelm 2014-03-05 proper UTF-8;
2014-02-28 traytel 2014-02-28 load Metis a little later
2014-02-28 nipkow 2014-02-28 added Rene Thiemann's patch for the nonterminating equality/subset test code for multisets
2014-02-18 kuncar 2014-02-18 simplify proofs because of the stronger reflexivity prover
2014-02-14 blanchet 2014-02-14 renamed 'enriched_type' to more informative 'functor' (following the renaming of enriched type constructors to bounded natural functors)
2014-02-12 blanchet 2014-02-12 adapted to 'xxx_{case,rec}' renaming, to new theorem names, and to new variable names in theorems * * * more transition of 'xxx_rec' to 'rec_xxx' and same for case * * * compile * * * 'rename_tac's to avoid referring to generated names * * * more robust scripts with 'rename_tac' * * * 'where' -> 'of' * * * 'where' -> 'of' * * * renamed 'xxx_rec' to 'rec_xxx'
2014-01-24 blanchet 2014-01-24 killed 'More_BNFs' by moving its various bits where they (now) belong
2013-12-27 haftmann 2013-12-27 prefer target-style syntaxx for sublocale
2013-11-10 haftmann 2013-11-10 qualifed popular user space names
2013-06-02 haftmann 2013-06-02 type class for confined subtraction
2013-04-04 haftmann 2013-04-04 sup on multisets
2013-04-03 haftmann 2013-04-03 default implementation of multisets by list with reasonable coverage of operations on multisets
2013-04-03 haftmann 2013-04-03 optionalized very specific code setup for multisets
2013-03-27 haftmann 2013-03-27 centralized various multiset operations in theory multiset; more conversions between multisets and lists respectively
2013-02-15 haftmann 2013-02-15 attempt to re-establish conventions which theories are loaded into the grand unified library theory; four different code generation tests for different code setup constellations; augment code generation setup where necessary
2013-02-15 haftmann 2013-02-15 two target language numeral types: integer and natural, as replacement for code_numeral; former theory HOL/Library/Code_Numeral_Types replaces HOL/Code_Numeral; refined stack of theories implementing int and/or nat by target language numerals; reduced number of target language numeral types to exactly one
2013-02-14 haftmann 2013-02-14 reform of predicate compiler / quickcheck theories: implement yieldn operations uniformly on the ML level -- predicate compiler uses negative integers as parameter to yieldn, whereas code_numeral represents natural numbers! avoid odd New_ prefix by joining related theories; avoid overcompact name DSequence; separated predicate inside random monad into separate theory; consolidated name of theory Quickcheck
2012-10-12 wenzelm 2012-10-12 discontinued obsolete typedef (open) syntax;
2012-10-11 haftmann 2012-10-11 avoid global interpretation
2012-10-11 haftmann 2012-10-11 simplified construction of fold combinator on multisets; more coherent name for fold combinator on multisets
2012-10-04 haftmann 2012-10-04 default simp rule for image under identity
2012-09-16 bulwahn 2012-09-16 removing find_theorems commands that were left in the developments accidently
2012-09-15 haftmann 2012-09-15 typeclass formalising bounded subtraction
2012-05-29 huffman 2012-05-29 add lemma set_of_image_mset
2012-05-29 huffman 2012-05-29 reordered sections
2012-05-29 huffman 2012-05-29 shortened yet more multiset proofs; added lemma size_multiset_of [simp]
2012-05-29 huffman 2012-05-29 remove unused intermediate lemma
2012-05-29 huffman 2012-05-29 shortened more multiset proofs
2012-05-29 huffman 2012-05-29 shortened some proofs
2012-05-29 huffman 2012-05-29 use transfer method for instance proof
2012-04-12 bulwahn 2012-04-12 multiset operations are defined with lift_definitions; tuned proofs;
2012-04-03 kuncar 2012-04-03 new package Lifting - initial commit
2012-03-29 kuncar 2012-03-29 use qualified names for rsp and rep_eq theorems in quotient_def
2012-03-28 bulwahn 2012-03-28 changing more definitions to quotient_definition
2012-03-28 bulwahn 2012-03-28 using abstract code equations for proofs of code equations in Multiset
2012-03-27 bulwahn 2012-03-27 association lists with distinct keys uses the quotient infrastructure to obtain code certificates; added remarks about further improvements