src/HOLCF/Tools/Domain/domain_take_proofs.ML
2010-05-05 ago farewell to old-style mem infixes -- type inference in situations with mem_int and mem_string should provide enough information to resolve the type of (op =)
2010-04-20 ago replace many uses of Drule.export_without_context with Drule.zero_var_indexes
2010-03-13 ago more consistent use of qualified bindings
2010-03-08 ago include take_info within take_induct_info type
2010-03-08 ago add type take_induct_info
2010-03-08 ago generate take_induct lemmas
2010-03-08 ago move proofs of reach and take lemmas to domain_take_proofs.ML
2010-03-08 ago add type take_info
2010-03-08 ago add function add_qualified_def
2010-03-05 ago remove dead code
2010-03-04 ago add function add_qualified_simp_thm
2010-03-03 ago generate lemma take_below, declare chain_take [simp]
2010-03-03 ago uniformly use variable names m and n in take-related lemmas; use export_without_context where appropriate
2010-03-03 ago move function mk_lub into holcf_library.ML
2010-03-02 ago move definition of finiteness predicate into domain_take_proofs.ML
2010-03-02 ago move take-related definitions and proofs to new module; simplify map_of_typ functions