| Tue, 21 Aug 2007 20:51:10 +0200 | huffman | add lemma of_int_power | changeset | files |
| Tue, 21 Aug 2007 20:50:12 +0200 | huffman | Isar-style proof for lfp_ordinal_induct | changeset | files |
| Tue, 21 Aug 2007 20:05:40 +0200 | wenzelm | ProofContext.restore_mode; | changeset | files |
| Tue, 21 Aug 2007 20:05:38 +0200 | wenzelm | added inner syntax mode, includes former type_mode and is_stmt; | changeset | files |