src/HOL/Library/Executable_Set.thy
2011-06-11 haftmann 2011-06-11 tuned comment
2010-11-22 haftmann 2010-11-22 replaced misleading Fset/fset name -- these do not stand for finite sets
2010-09-04 haftmann 2010-09-04 added more explicit warning
2010-08-10 haftmann 2010-08-10 executable relation operations contributed by Tjark Weber
2010-06-28 haftmann 2010-06-28 dropped ancient infix mem; refined code generation operations in List.thy
2010-05-20 haftmann 2010-05-20 renamed List_Set to the now more appropriate More_Set
2010-05-20 haftmann 2010-05-20 added theory More_List
2010-04-16 wenzelm 2010-04-16 replaced generic 'hide' command by more conventional 'hide_class', 'hide_type', 'hide_const', 'hide_fact' -- frees some popular keywords;
2010-01-31 haftmann 2010-01-31 adjusted to changes in List_Set.thy
2009-12-07 haftmann 2009-12-07 merged
2009-12-07 haftmann 2009-12-07 merged Crude_Executable_Set into Executable_Set
2009-10-26 haftmann 2009-10-26 added SML_Quickcheck import
2009-10-06 haftmann 2009-10-06 added Coset as constructor
2009-09-25 haftmann 2009-09-25 merged
2009-09-23 haftmann 2009-09-23 explicitly hide empty, inter, union
2009-09-23 haftmann 2009-09-23 merged
2009-09-19 haftmann 2009-09-19 inter and union are mere abbreviations for inf and sup
2009-09-24 haftmann 2009-09-24 subsumed by more general setup in List.thy
2009-09-23 haftmann 2009-09-23 hide newly introduced constants
2009-09-18 haftmann 2009-09-18 INTER and UNION are mere abbreviations for INFI and SUPR
2009-09-16 haftmann 2009-09-16 Inter and Union are mere abbreviations for Inf and Sup
2009-07-22 haftmann 2009-07-22 moved complete_lattice &c. into separate theory
2009-07-14 haftmann 2009-07-14 code attributes use common underscore convention
2009-06-29 haftmann 2009-06-29 Executable_Set is now a simple wrapper around Fset
2009-06-28 haftmann 2009-06-28 Executable_Set now based on Code_Set
2009-03-23 haftmann 2009-03-23 Main is (Complex_Main) base entry point in library theories
2009-03-05 haftmann 2009-03-05 set operations Int, Un, INTER, UNION, Inter, Union, empty, UNIV are now proper qualified constants with authentic syntax
2008-12-15 nipkow 2008-12-15 flipped fold implementation
2008-12-11 nipkow 2008-12-11 code for {x:A. P(x)} and for fold
2008-12-01 haftmann 2008-12-01 added code equation for subset
2008-10-07 haftmann 2008-10-07 only one theorem table for both code generators
2008-07-07 haftmann 2008-07-07 absolute imports of HOL/*.thy theories
2008-06-26 haftmann 2008-06-26 established Plain theory and image
2008-05-07 berghofe 2008-05-07 - Declared subset_eq as code lemma - Deleted types_code declaration for sets
2008-03-17 wenzelm 2008-03-17 avoid rebinding of existing facts;
2008-01-10 berghofe 2008-01-10 New interface for test data generators.
2007-12-10 haftmann 2007-12-10 switched import from Main to List
2007-08-24 haftmann 2007-08-24 overloaded definitions accompanied by explicit constants
2007-07-19 haftmann 2007-07-19 uniform naming conventions for CG theories