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