Thu, 07 Apr 2011 14:51:28 +0200 | bulwahn | removing decrement of cardinality in quickcheck -- counting cardinalities starts at 1 | changeset | files |
Thu, 07 Apr 2011 14:51:26 +0200 | bulwahn | removing instantiation exhaustive for unit in Quickcheck_Exhaustive | changeset | files |
Thu, 07 Apr 2011 14:51:25 +0200 | bulwahn | correcting bounded_forall construction; tuned | changeset | files |
Thu, 07 Apr 2011 13:01:27 +0200 | haftmann | dropped unused lemmas; proper Isar proof | changeset | files |
Thu, 07 Apr 2011 12:16:27 +0200 | blanchet | further development of new Skolemizer -- make sure constructed terms have correct types and fixed a few bugs where the goal was out of sync with what we had in mind | changeset | files |
Thu, 07 Apr 2011 12:16:26 +0200 | blanchet | make new Skolemizer more robust | changeset | files |
Thu, 07 Apr 2011 12:16:25 +0200 | blanchet | tuned comment | changeset | files |