Wed, 07 Jul 2010 08:25:21 +0200 | bulwahn | added the new command inductive_cases to derive simplification equations for inductive predicates; added binding simps for general simplification equation | changeset | files |
Tue, 06 Jul 2010 08:08:35 -0700 | huffman | merged | changeset | files |
Mon, 05 Jul 2010 09:14:51 -0700 | huffman | generalize type of is_interval to class euclidean_space | changeset | files |