Wed, 13 Jun 2007 10:43:38 +0200 | wenzelm | tuned proofs: avoid implicit prems; | changeset | files |
Wed, 13 Jun 2007 03:31:11 +0200 | huffman | removed constant int :: nat => int; | changeset | files |
Wed, 13 Jun 2007 03:28:21 +0200 | huffman | thm antiquotations | changeset | files |
Wed, 13 Jun 2007 00:02:06 +0200 | wenzelm | transaction: context_position (non-destructive only); | changeset | files |
Wed, 13 Jun 2007 00:02:05 +0200 | wenzelm | added map_current; | changeset | files |
Wed, 13 Jun 2007 00:02:04 +0200 | wenzelm | tuned msg; | changeset | files |
Wed, 13 Jun 2007 00:02:03 +0200 | wenzelm | apply_method/end_proof: pass position; | changeset | files |