Mon, 01 Mar 2010 17:32:23 -0800 | huffman | add lemmas about ssum_map and sprod_map | changeset | files |
Mon, 01 Mar 2010 16:58:16 -0800 | huffman | generate take_take rules | changeset | files |
Mon, 01 Mar 2010 16:36:25 -0800 | huffman | add function define_take_functions | changeset | files |
Mon, 01 Mar 2010 11:15:18 -0800 | huffman | add missing strictify rule to proof script | changeset | files |
Mon, 01 Mar 2010 10:00:14 -0800 | huffman | qualify constructor names with type name | changeset | files |
Mon, 01 Mar 2010 09:55:32 -0800 | huffman | move definition of case combinator to domain_constructors.ML | changeset | files |