2010-04-20 huffman 2010-04-20 replace many uses of Drule.export_without_context with Drule.zero_var_indexes
2010-04-12 huffman 2010-04-12 for axiomatic domain package, declare types and arities in domain_axioms.ML instead of domain_extender.ML
2010-03-22 wenzelm 2010-03-22 eliminated old-style Drule.add_axiom in favour of Specification.axiom, with explicit Drule.export_without_context to imitate the old behaviour;
2010-03-22 wenzelm 2010-03-22 replaced PureThy.add_axioms by more basic Drule.add_axiom, which is old-style nonetheless;
2010-03-14 huffman 2010-03-14 old domain package also defines map functions
2010-03-13 huffman 2010-03-13 more consistent use of qualified bindings
2010-03-08 huffman 2010-03-08 include take_info within take_induct_info type
2010-03-08 huffman 2010-03-08 pass take_info as an argument to comp_theorems
2010-03-08 huffman 2010-03-08 pass take_induct_info as an argument to comp_theorems
2010-03-08 huffman 2010-03-08 move proofs of reach and take lemmas to domain_take_proofs.ML
2010-03-03 huffman 2010-03-03 add infix declarations
2010-03-03 huffman 2010-03-03 remove copy_of_dtyp from domain_axioms.ML
2010-03-03 huffman 2010-03-03 add_axioms returns an iso_info; add_theorems takes an iso_info as an argument
2010-03-03 huffman 2010-03-03 add function axiomatize_lub_take
2010-03-02 huffman 2010-03-02 simplify add_axioms function; remove obsolete domain_syntax.ML
2010-03-02 huffman 2010-03-02 proper names for types cfun, sprod, ssum
2010-03-02 huffman 2010-03-02 add_axioms no longer needs a definitional mode
2010-03-02 huffman 2010-03-02 move definition of finiteness predicate into domain_take_proofs.ML
2010-03-02 huffman 2010-03-02 move take-related definitions and proofs to new module; simplify map_of_typ functions
2010-03-02 huffman 2010-03-02 remove map_tab argument to calc_axioms
2010-03-02 huffman 2010-03-02 UNIV is not a logical constant
2010-03-02 huffman 2010-03-02 re-enable bisim code, now in domain_theorems.ML
2010-03-02 huffman 2010-03-02 remove dead code
2010-03-02 huffman 2010-03-02 domain package no longer generates copy functions; all proofs use take functions instead
2010-03-01 huffman 2010-03-01 move definition of case combinator to domain_constructors.ML
2010-02-28 huffman 2010-02-28 move definition and syntax of pattern combinators into domain_constructors.ML
2010-02-27 huffman 2010-02-27 register match functions from domain_constructors.ML
2010-02-27 huffman 2010-02-27 move definition of match combinators to domain_constructors.ML
2010-02-27 huffman 2010-02-27 move definition of discriminators to domain_constructors.ML
2010-02-25 huffman 2010-02-25 rewrite domain package code for selector functions
2010-02-24 huffman 2010-02-24 reorganizing domain package code (in progress)
2010-02-22 huffman 2010-02-22 add mixfix field to type Domain_Library.cons
2009-12-04 haftmann 2009-12-04 modernized structure Datatype_Aux
2009-11-19 huffman 2009-11-19 store map_ID thms in theory data; automate proofs of reach lemmas
2009-11-19 huffman 2009-11-19 domain_isomorphism package defines combined copy function
2009-11-19 huffman 2009-11-19 domain_isomorphism package defines copy functions
2009-11-19 huffman 2009-11-19 copy_of_dtyp uses map table from theory data
2009-11-19 huffman 2009-11-19 clean up indentation; add 'definitional' option flag
2009-11-05 huffman 2009-11-05 map functions for various types, with ep_pair/deflation/finite_deflation lemmas
2009-11-02 huffman 2009-11-02 domain package no longer uses cfst/csnd/cpair
2009-10-29 wenzelm 2009-10-29 standardized filter/filter_out;
2009-10-27 wenzelm 2009-10-27 eliminated some old folds;
2009-10-15 wenzelm 2009-10-15 replaced String.concat by implode; replaced String.concatWith by space_implode; replaced (Seq.flat o by Seq.maps; replaced List.mapPartial by map_filter; replaced List.concat by flat; replaced (flat o map) by maps, which produces less garbage;
2009-07-21 haftmann 2009-07-21 obey captialized directory names convention