| Thu, 02 Oct 2014 17:39:38 +0200 | blanchet | avoid duplicate 'obtain' in veriT Isar proofs, by removing dubious condition | changeset | files |
| Thu, 02 Oct 2014 15:24:51 +0200 | blanchet | eliminate duplicate hypotheses (which can arise due to (un)clausification) | changeset | files |
| Thu, 02 Oct 2014 11:33:08 +0200 | haftmann | formal lcm definition for polynomials | changeset | files |
| Thu, 02 Oct 2014 11:33:06 +0200 | haftmann | moved lemmas out of Int.thy which have nothing to do with int | changeset | files |
| Thu, 02 Oct 2014 11:33:05 +0200 | haftmann | redundant: dropped | changeset | files |
| Thu, 02 Oct 2014 11:33:04 +0200 | haftmann | tuned Heap_Monad.successE | changeset | files |
| Thu, 02 Oct 2014 12:02:29 +0200 | blanchet | documentation | changeset | files |