src/HOLCF/Tools/Domain/domain_take_proofs.ML
2010-05-05 haftmann 2010-05-05 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 huffman 2010-04-20 replace many uses of Drule.export_without_context with Drule.zero_var_indexes
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 add type take_induct_info
2010-03-08 huffman 2010-03-08 generate take_induct lemmas
2010-03-08 huffman 2010-03-08 move proofs of reach and take lemmas to domain_take_proofs.ML
2010-03-08 huffman 2010-03-08 add type take_info
2010-03-08 huffman 2010-03-08 add function add_qualified_def
2010-03-05 huffman 2010-03-05 remove dead code
2010-03-04 huffman 2010-03-04 add function add_qualified_simp_thm
2010-03-03 huffman 2010-03-03 generate lemma take_below, declare chain_take [simp]
2010-03-03 huffman 2010-03-03 uniformly use variable names m and n in take-related lemmas; use export_without_context where appropriate
2010-03-03 huffman 2010-03-03 move function mk_lub into holcf_library.ML
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