| Thu, 18 Aug 2005 11:17:40 +0200 | wenzelm | added map_specs/facts operators (from locale.ML); | changeset | files |
| Thu, 18 Aug 2005 11:17:39 +0200 | wenzelm | removed obsolete Theory.sign_of; | changeset | files |
| Thu, 18 Aug 2005 11:17:38 +0200 | wenzelm | load method.ML before proof.ML; | changeset | files |
| Thu, 18 Aug 2005 11:17:37 +0200 | wenzelm | added interfaces for compile translation functions (from Isar/isar_thy.ML); | changeset | files |
| Thu, 18 Aug 2005 11:17:36 +0200 | wenzelm | added tap; | changeset | files |
| Thu, 18 Aug 2005 11:17:35 +0200 | wenzelm | updated; | changeset | files |
| Thu, 18 Aug 2005 11:17:34 +0200 | wenzelm | usedir: tuned option -V; | changeset | files |
| Thu, 18 Aug 2005 11:17:33 +0200 | wenzelm | usedir: removed option -H; | changeset | files |
| Thu, 18 Aug 2005 11:17:32 +0200 | wenzelm | * Proper output of proof terms within a proof context; | changeset | files |
| Wed, 17 Aug 2005 17:04:15 +0200 | ballarin | Improved generation of witnesses in interpretation. | changeset | files |
| Wed, 17 Aug 2005 17:03:20 +0200 | ballarin | Interpretation in locales. | changeset | files |
| Wed, 17 Aug 2005 17:02:16 +0200 | ballarin | Use interpretation in locales. | changeset | files |
| Wed, 17 Aug 2005 15:10:00 +0200 | paulson | new examples | changeset | files |
| Wed, 17 Aug 2005 14:19:17 +0200 | nipkow | *** empty log message *** | changeset | files |
| Wed, 17 Aug 2005 13:52:53 +0200 | paulson | new command to invoke ATPs | changeset | files |
| Wed, 17 Aug 2005 11:44:02 +0200 | nipkow | small mods to code lemmas | changeset | files |
| Wed, 17 Aug 2005 11:15:23 +0200 | wenzelm | made SML/XL happy; | changeset | files |
| Wed, 17 Aug 2005 08:06:12 +0200 | nipkow | list_all_conv -> iff | changeset | files |
| Tue, 16 Aug 2005 19:25:42 +0200 | nipkow | name fix | changeset | files |
| Tue, 16 Aug 2005 19:25:32 +0200 | nipkow | added quite a few functions for code generation | changeset | files |
| Tue, 16 Aug 2005 18:53:11 +0200 | paulson | more simprules now have names | changeset | files |
| Tue, 16 Aug 2005 15:36:28 +0200 | paulson | classical rules must have names for ATP integration | changeset | files |
| Tue, 16 Aug 2005 13:54:24 +0200 | nipkow | added listT | changeset | files |
| Tue, 16 Aug 2005 13:42:53 +0200 | wenzelm | support for document versions; | changeset | files |
| Tue, 16 Aug 2005 13:42:52 +0200 | wenzelm | eliminated datatype token; | changeset | files |
| Tue, 16 Aug 2005 13:42:51 +0200 | wenzelm | begin_index: list of docs; | changeset | files |
| Tue, 16 Aug 2005 13:42:50 +0200 | wenzelm | added eq_syntax; | changeset | files |
| Tue, 16 Aug 2005 13:42:49 +0200 | wenzelm | export proof_syntax, proof_of; | changeset | files |