src/HOLCF/Tools/Domain/domain_constructors.ML
2010-05-28 ago made SML/NJ quite happy;
2010-05-24 ago move unused pattern match syntax stuff into HOLCF/ex
2010-05-24 ago rename type 'a maybe to 'a match; rename Fixrec.return to Fixrec.succeed
2010-05-22 ago domain package internal proofs use fixed set of continuity rules, rather than taking cont2cont rules from context
2010-05-19 ago remove unnecessary constant Fixrec.bind
2010-04-20 ago replace many uses of Drule.export_without_context with Drule.zero_var_indexes
2010-03-14 ago move functions into holcf_library.ML
2010-03-14 ago simplify definition of when combinators
2010-03-13 ago renamed some lemmas generated by the domain package
2010-03-13 ago pass binding as argument to add_domain_constructors; proper binding for case combinator
2010-03-03 ago add infix declarations
2010-03-02 ago use y as variable name in casedist, like datatype package
2010-03-02 ago move take-related definitions and proofs to new module; simplify map_of_typ functions
2010-03-02 ago add missing rule to case_strict proof script
2010-03-01 ago add missing strictify rule to proof script
2010-03-01 ago qualify constructor names with type name
2010-03-01 ago move definition of case combinator to domain_constructors.ML
2010-03-01 ago remove dependence on Domain_Library
2010-03-01 ago more uses of function get_vars
2010-03-01 ago add functions get_vars, get_vars_avoiding
2010-03-01 ago move proofs of pat_rews to domain_constructors.ML
2010-02-28 ago add_domain_constructors takes iso_info record as argument
2010-02-28 ago fix infix declarations
2010-02-28 ago move common functions into new file holcf_library.ML
2010-02-28 ago move case combinator syntax to domain_constructors.ML
2010-02-28 ago use correct syntax name for pattern combinator
2010-02-28 ago move definition and syntax of pattern combinators into domain_constructors.ML
2010-02-27 ago move proofs of match_rews to domain_constructors.ML
2010-02-27 ago register match functions from domain_constructors.ML
2010-02-27 ago move definition of match combinators to domain_constructors.ML
2010-02-27 ago move proofs of dis_rews to domain_constructors.ML; change dis_defins to iff-style
2010-02-27 ago move definition of discriminators to domain_constructors.ML
2010-02-27 ago move proofs of when_rews intro domain_constructors.ML
2010-02-27 ago moved proofs of dist_les and dist_eqs to domain_constructors.ML
2010-02-27 ago move proofs of casedist into domain_constructors.ML
2010-02-26 ago move proofs of injects and inverts to domain_constructors.ML
2010-02-26 ago reuse vars_of function
2010-02-26 ago remove unnecessary stuff from argument to add_constructors function
2010-02-26 ago reorder sections
2010-02-26 ago move proof of con_rews into domain_constructor.ML
2010-02-26 ago don't bother returning con_defs
2010-02-26 ago move constructor-specific stuff to a separate function
2010-02-26 ago replace prove_thm function
2010-02-26 ago move proof of compactness rules into domain_constructors.ML
2010-02-26 ago add some convenience functions
2010-02-25 ago rewrite domain package code for selector functions
2010-02-24 ago add function beta_of_def
2010-02-24 ago reorganizing domain package code (in progress)