Tue, 12 Jul 2005 18:26:44 +0200 | huffman | added lemmas sfst_defined_iff, ssnd_defined_iff, sfst_defined, ssnd_defined | changeset | files |
Tue, 12 Jul 2005 18:20:44 +0200 | huffman | generalized types of monadic operators to class cpo; added match function for UU | changeset | files |
Tue, 12 Jul 2005 17:56:03 +0200 | avigad | added lemmas to OrderedGroup.thy (reasoning about signs, absolute value, triangle inequalities) | changeset | files |
Tue, 12 Jul 2005 12:49:46 +0200 | paulson | experimental code to reduce the amount of type information in blast | changeset | files |
Tue, 12 Jul 2005 12:49:00 +0200 | paulson | tweaked | changeset | files |
Tue, 12 Jul 2005 11:55:33 +0200 | berghofe | Added \<module> symbol. | changeset | files |