Wed, 31 Mar 2010 16:44:41 +0200 | bulwahn | adding MREC induction rule in Imperative HOL | changeset | files |
Wed, 31 Mar 2010 16:44:41 +0200 | bulwahn | made smlnj happy | changeset | files |
Wed, 31 Mar 2010 16:44:41 +0200 | bulwahn | adding examples of function predicate replacement and arithmetic examples for the predicate compiler; tuned | changeset | files |