| Thu, 14 Jun 2007 07:27:55 +0200 |
nipkow |
fixed filter syntax
|
changeset |
files
|
| Thu, 14 Jun 2007 00:48:42 +0200 |
wenzelm |
updated 'find_theorems' -- moved ProofGeneral specifics to ProofGeneral/CHANGES;
|
changeset |
files
|
| Thu, 14 Jun 2007 00:22:45 +0200 |
wenzelm |
tuned proofs: avoid implicit prems;
|
changeset |
files
|
| Wed, 13 Jun 2007 19:14:51 +0200 |
huffman |
int abbreviates of_nat
|
changeset |
files
|
| Wed, 13 Jun 2007 18:30:17 +0200 |
wenzelm |
tuned proofs: avoid implicit prems;
|
changeset |
files
|
| Wed, 13 Jun 2007 18:30:16 +0200 |
wenzelm |
tuned proofs: avoid implicit prems;
|
changeset |
files
|
| Wed, 13 Jun 2007 18:30:15 +0200 |
wenzelm |
tuned comments;
|
changeset |
files
|
| 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
|