| Fri, 28 May 2010 17:00:38 +0200 | blanchet | merged | changeset | files |
| Fri, 28 May 2010 13:49:21 +0200 | blanchet | make sure chained facts appear in Isar proofs generated by Sledgehammer -- otherwise the proof won't work | changeset | files |
| Thu, 27 May 2010 17:22:16 +0200 | blanchet | Nitpick: show "..." in datatype values (e.g., [{0::nat, ...}]), since these are really equivalence classes | changeset | files |