2010-10-14 huffman 2010-10-14 include iso_info as part of constr_info type
2010-10-14 huffman 2010-10-14 remove function Domain_Theorems.theorems; bind theorem names directly from Domain_Constructors.add_domain_constructors
2010-10-08 huffman 2010-10-08 rename class 'sfp' to 'bifinite'
2010-10-06 huffman 2010-10-06 major reorganization/simplification of HOLCF type classes: removed profinite/bifinite classes and approx function; universal domain uses approx_chain locale instead of bifinite class; ideal_completion locale does not use 'take' functions, requires countable basis instead; replaced type 'udom alg_defl' with type 'sfp'; replaced class 'rep' with class 'sfp'; renamed REP('a) to SFP('a);
2010-09-30 huffman 2010-09-30 new_domain emits proper error message when a constructor argument type does not have sort 'rep'
2010-09-20 wenzelm 2010-09-20 renamed structure PureThy to Pure_Thy and moved most content to Global_Theory, to emphasize that this is global-only;
2010-05-17 wenzelm 2010-05-17 prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax; eliminated old-style structure aliases K = Keyword, P = Parse;
2010-04-12 huffman 2010-04-12 remove dead code
2010-04-12 huffman 2010-04-12 share more code between definitional and axiomatic domain packages
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-19 wenzelm 2010-03-19 OuterParse.type_args_constrained;
2010-03-14 huffman 2010-03-14 use headers consistently
2010-03-13 huffman 2010-03-13 pass domain binding as argument to Domain_Theorems.theorems; proper qualified bindings for theorem names
2010-03-13 huffman 2010-03-13 pass take_info as argument to Domain_Theorems.theorems
2010-03-13 huffman 2010-03-13 replace some string arguments with 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-03 huffman 2010-03-03 add_axioms returns an iso_info; add_theorems takes an iso_info as an argument
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 remove unused mixfix component from type cons
2010-03-02 huffman 2010-03-02 cleaned up, added type annotations
2010-03-02 huffman 2010-03-02 remove unused selector field from type arg
2010-03-02 huffman 2010-03-02 add_syntax no longer needs a definitional mode
2010-03-02 huffman 2010-03-02 add_axioms no longer needs a definitional mode
2010-03-02 huffman 2010-03-02 get rid of primes on thy variables
2010-03-02 huffman 2010-03-02 merged
2010-03-02 huffman 2010-03-02 re-enable bisim code, now in domain_theorems.ML
2010-03-02 huffman 2010-03-02 domain package no longer generates copy functions; all proofs use take functions instead
2010-02-27 huffman 2010-02-27 domain_isomorphism function returns iso_info record
2010-02-24 huffman 2010-02-24 reorganizing domain package code (in progress)
2010-02-24 huffman 2010-02-24 change domain package's treatment of variable names in theorems to be like datatype package
2010-02-24 wenzelm 2010-02-24 allow general mixfix syntax for type constructors;
2010-02-22 huffman 2010-02-22 add mixfix field to type Domain_Library.cons
2010-02-15 wenzelm 2010-02-15 discontinued unnamed infix syntax;
2009-12-19 huffman 2009-12-19 add 'morphisms' option to domain_isomorphism command
2009-12-04 haftmann 2009-12-04 modernized structure Datatype_Aux
2009-11-25 haftmann 2009-11-25 normalized uncurry take/drop
2009-11-24 haftmann 2009-11-24 curried take/drop
2009-11-19 huffman 2009-11-19 clean up indentation; add 'definitional' option flag
2009-11-19 huffman 2009-11-19 clean up indentation
2009-10-21 haftmann 2009-10-21 dropped redundant gen_ prefix
2009-10-20 haftmann 2009-10-20 replaced old_style infixes eq_set, subset, union, inter and variants by generic versions
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