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
2012-03-14 wenzelm 2012-03-14 some proof indentation;
2012-03-02 bulwahn 2012-03-02 adding finiteness of intervals on integer sets; adding another finiteness theorem for multisets
2012-02-28 wenzelm 2012-02-28 tuned proofs;
2012-02-01 bulwahn 2012-02-01 improving code equations for multisets that violated the distinct AList abstraction
2012-01-17 bulwahn 2012-01-17 renaming theory AList_Impl back to AList (reverting 1fec5b365f9b; AList with distinct key invariant is called DAList)
2012-01-17 bulwahn 2012-01-17 renamed theory AList to DAList
2012-01-10 bulwahn 2012-01-10 improving code generation for multisets; adding exhaustive quickcheck generators for multisets
2011-12-26 haftmann 2011-12-26 moved theorem requiring multisets from More_List to Multiset
2011-12-14 bulwahn 2011-12-14 adding code attribute to enable evaluation of equality on multisets
2011-11-30 wenzelm 2011-11-30 prefer typedef without extra definition and alternative name; tuned proofs;
2011-11-20 wenzelm 2011-11-20 eliminated obsolete "standard";
2011-09-12 nipkow 2011-09-12 new fastforce replacing fastsimp - less confusing name