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
2011-08-20 wenzelm 2011-08-20 odd workaround for odd problem of load order in HOL/ex/ROOT.ML (!??);
2011-05-20 haftmann 2011-05-20 names of fold_set locales resemble name of characteristic property more closely
2011-05-14 haftmann 2011-05-14 use pointfree characterisation for fold_set locale
2011-01-11 haftmann 2011-01-11 "enriched_type" replaces less specific "type_lifting"
2010-12-21 haftmann 2010-12-21 tuned type_lifting declarations
2010-12-07 haftmann 2010-12-07 name filter operation just filter (c.f. List.filter and list comprehension syntax)
2010-12-06 haftmann 2010-12-06 replace `type_mapper` by the more adequate `type_lifting`
2010-12-03 haftmann 2010-12-03 lemma multiset_of_rev
2010-11-18 haftmann 2010-11-18 mapper for mulitset type
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-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 multiset_of_filter, sort_key_by_quicksort
2010-10-29 Lars Noschinski 2010-10-29 merged
2010-09-22 Lars Noschinski 2010-09-22 Remove unnecessary premise of mult1_union