| Fri, 28 May 2010 18:15:53 +0200 | wenzelm | merged | changeset | files |
| 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 |
| Thu, 27 May 2010 16:42:03 +0200 | blanchet | make Nitpick "show_all" option behave less surprisingly | changeset | files |
| Fri, 28 May 2010 13:37:47 +0200 | haftmann | merged | changeset | files |
| Fri, 28 May 2010 13:37:29 +0200 | haftmann | avoid reference to thm PairE | changeset | files |