Tue, 01 Jul 2014 16:49:25 +0200 | blanchet | fixed soundness bug in monotonicity-based type encodings -- the helper facts must be considered too | changeset | files |
Tue, 01 Jul 2014 16:47:10 +0200 | blanchet | added hidden check to Sledgehammer fact filters, to avoid picking up facts like 'Nat.nat_induct0' | changeset | files |
Tue, 01 Jul 2014 16:47:10 +0200 | blanchet | whitespace tuning | changeset | files |