| Wed, 13 Jun 2007 18:30:11 +0200 | wenzelm | tuned proofs: avoid implicit prems; | changeset | files |
| Wed, 13 Jun 2007 16:43:02 +0200 | huffman | clean up instance proofs; reorganize section headings | changeset | files |
| Wed, 13 Jun 2007 14:21:54 +0200 | wenzelm | reactivated theory Class; | changeset | files |
| Wed, 13 Jun 2007 12:22:02 +0200 | urbanc | added the Q_Unit rule (was missing) and adjusted the proof accordingly | changeset | files |
| Wed, 13 Jun 2007 11:54:03 +0200 | wenzelm | * Isar: method "assumption" (implicit closing of subproofs) takes non-atomic goal assumptions into account; | changeset | files |
| Wed, 13 Jun 2007 11:16:24 +0200 | narboux | generate_fresh works even if there is no free variable in the goal | changeset | files |
| Wed, 13 Jun 2007 10:44:35 +0200 | wenzelm | tuned; | changeset | files |
| Wed, 13 Jun 2007 10:43:38 +0200 | wenzelm | tuned proofs: avoid implicit prems; | changeset | files |