| Tue, 01 Jul 2014 16:09:51 +0100 | paulson | Merge | changeset | files |
| Tue, 01 Jul 2014 16:08:31 +0100 | paulson | for new release | changeset | files |
| Tue, 01 Jul 2014 17:06:54 +0200 | desharna | merge | changeset | files |
| Tue, 01 Jul 2014 17:01:48 +0200 | desharna | document property 'rel_induct' | changeset | files |
| Tue, 01 Jul 2014 17:01:28 +0200 | desharna | generate 'rel_induct' theorem for datatypes | changeset | files |
| 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 |