| Sun, 28 Aug 2005 19:48:15 +0200 | wenzelm | output \<^loc> as 'loc' span; | changeset | files |
| Sun, 28 Aug 2005 19:47:24 +0200 | wenzelm | isatool latex -o sty; | changeset | files |
| Sun, 28 Aug 2005 19:46:49 +0200 | wenzelm | added 'loc'; | changeset | files |
| Sun, 28 Aug 2005 19:42:19 +0200 | wenzelm | updated; | changeset | files |
| Sun, 28 Aug 2005 19:42:10 +0200 | wenzelm | ASCII back-quote no longer sym char; | changeset | files |
| Sun, 28 Aug 2005 16:35:39 +0200 | wenzelm | added \isactrlloc; | changeset | files |
| Sun, 28 Aug 2005 16:06:07 +0200 | wenzelm | * ML functions legacy_bindings and use_legacy_bindings; | changeset | files |
| Sun, 28 Aug 2005 16:04:55 +0200 | wenzelm | avoid symbolic identifier; | changeset | files |
| Sun, 28 Aug 2005 16:04:54 +0200 | wenzelm | added (use_)legacy_bindings; | changeset | files |
| Sun, 28 Aug 2005 16:04:53 +0200 | wenzelm | output_basic: handle AltString token; | changeset | files |
| Sun, 28 Aug 2005 16:04:52 +0200 | wenzelm | removed obsolete type_syn; | changeset | files |
| Sun, 28 Aug 2005 16:04:51 +0200 | wenzelm | unskolem local vars; | changeset | files |
| Sun, 28 Aug 2005 16:04:50 +0200 | wenzelm | tuned; | changeset | files |
| Sun, 28 Aug 2005 16:04:49 +0200 | wenzelm | added alt_string; | changeset | files |
| Sun, 28 Aug 2005 16:04:48 +0200 | wenzelm | added AltString token (delimited by ASCII back-quotes); | changeset | files |
| Sun, 28 Aug 2005 16:04:47 +0200 | wenzelm | removed unused dest operation; | changeset | files |
| Sun, 28 Aug 2005 16:04:46 +0200 | wenzelm | export theorems_of; | changeset | files |
| Sun, 28 Aug 2005 16:04:45 +0200 | wenzelm | tuned some proofs; | changeset | files |
| Sun, 28 Aug 2005 16:04:44 +0200 | wenzelm | removed obsolete arities; | changeset | files |
| Sun, 28 Aug 2005 16:04:43 +0200 | wenzelm | tuned size of included graph; | changeset | files |
| Sun, 28 Aug 2005 16:04:42 +0200 | wenzelm | added \isachardoublequoteopen/close, \isacharbackquoteopen/close; | changeset | files |
| Sun, 28 Aug 2005 10:08:36 +0200 | haftmann | (branch cleanup) | changeset | files |
| Sun, 28 Aug 2005 10:05:03 +0200 | haftmann | (allocating new branch) | changeset | files |
| Sun, 28 Aug 2005 09:36:18 +0200 | haftmann | added superclasses, class_le_path | changeset | files |
| Sun, 28 Aug 2005 09:26:22 +0200 | haftmann | added alist.ML | changeset | files |
| Sun, 28 Aug 2005 09:18:22 +0200 | haftmann | added 'these', removed assoc2 | changeset | files |
| Sun, 28 Aug 2005 09:02:42 +0200 | haftmann | added alist module | changeset | files |
| Fri, 26 Aug 2005 19:47:23 +0200 | berghofe | Fixed bug. | changeset | files |
| Fri, 26 Aug 2005 19:36:07 +0200 | quigley | DFG output now works for untyped rules (ML "ResClause.untyped();") | changeset | files |
| Fri, 26 Aug 2005 10:01:06 +0200 | ballarin | Lemmas on dvd, power and finite summation added or strengthened. | changeset | files |
| Fri, 26 Aug 2005 08:42:52 +0200 | haftmann | replaced '?' by '??' | changeset | files |
| Thu, 25 Aug 2005 17:51:11 +0200 | berghofe | Adapted to new code generator syntax. | changeset | files |
| Thu, 25 Aug 2005 16:17:40 +0200 | berghofe | Put quotation marks around some occurrences of "file", since it is now | changeset | files |
| Thu, 25 Aug 2005 16:13:09 +0200 | berghofe | Adapted to new code generator syntax. | changeset | files |
| Thu, 25 Aug 2005 16:10:16 +0200 | berghofe | Implemented incremental code generation. | changeset | files |
| Thu, 25 Aug 2005 09:29:05 +0200 | haftmann | fixed typo | changeset | files |
| Thu, 25 Aug 2005 09:25:03 +0200 | haftmann | add_locale_context(_i) now exporting elements (still some refinements to be done) | changeset | files |
| Thu, 25 Aug 2005 09:23:40 +0200 | haftmann | added ? combinator for conditional transformations | changeset | files |
| Thu, 25 Aug 2005 09:23:13 +0200 | haftmann | added 'default' function | changeset | files |
| Wed, 24 Aug 2005 12:07:00 +0200 | ballarin | Printing of interpretations: option to show witness theorems; | changeset | files |
| Wed, 24 Aug 2005 12:05:48 +0200 | ballarin | Interpretation in locales: extended back end; | changeset | files |
| Tue, 23 Aug 2005 09:18:44 +0200 | haftmann | replaced ? by ?? | changeset | files |
| Fri, 19 Aug 2005 23:20:50 +0200 | wenzelm | fixed deps; | changeset | files |
| Fri, 19 Aug 2005 22:50:20 +0200 | wenzelm | tuned arrangement of generated stuff; | changeset | files |
| Fri, 19 Aug 2005 22:44:36 +0200 | wenzelm | updated; | changeset | files |
| Fri, 19 Aug 2005 22:44:01 +0200 | wenzelm | tuned generated stuff; | changeset | files |
| Fri, 19 Aug 2005 22:28:23 +0200 | wenzelm | updated; | changeset | files |
| Fri, 19 Aug 2005 22:28:23 +0200 | wenzelm | updated; | changeset | files |
| Fri, 19 Aug 2005 22:25:21 +0200 | wenzelm | obsolete; | changeset | files |
| Fri, 19 Aug 2005 22:25:14 +0200 | wenzelm | tuned; | changeset | files |
| Fri, 19 Aug 2005 22:19:59 +0200 | wenzelm | updated; | changeset | files |
| Fri, 19 Aug 2005 18:38:59 +0200 | nipkow | *** empty log message *** | changeset | files |
| Fri, 19 Aug 2005 11:03:06 +0200 | wenzelm | updated; | changeset | files |
| Fri, 19 Aug 2005 10:50:05 +0200 | wenzelm | updated; | changeset | files |
| Fri, 19 Aug 2005 09:40:44 +0200 | nipkow | -H deleted | changeset | files |
| Fri, 19 Aug 2005 09:29:58 +0200 | nipkow | ML_idf -> ML | changeset | files |
| Thu, 18 Aug 2005 13:09:40 +0200 | paulson | nicer list of axioms used | changeset | files |
| Thu, 18 Aug 2005 13:09:21 +0200 | paulson | no need for TPTP2X unless SPASS is used | changeset | files |
| Thu, 18 Aug 2005 13:06:05 +0200 | paulson | optimization to incr_indexes? | changeset | files |
| Thu, 18 Aug 2005 12:11:06 +0200 | wenzelm | tuned; | changeset | files |
| Thu, 18 Aug 2005 12:07:33 +0200 | wenzelm | fixed command prompt (was broken due to P.tags); | changeset | files |
| Thu, 18 Aug 2005 11:59:17 +0200 | wenzelm | * The ML antiquotation prints type-checked ML expressions verbatim. | changeset | files |
| Thu, 18 Aug 2005 11:17:51 +0200 | wenzelm | replace freeze by 'setmp show_question_marks false'; | changeset | files |
| Thu, 18 Aug 2005 11:17:50 +0200 | wenzelm | proof_to_theory_context: interaction flag; | changeset | files |
| Thu, 18 Aug 2005 11:17:49 +0200 | wenzelm | accomodate interface Proof vs. Method; | changeset | files |
| Thu, 18 Aug 2005 11:17:48 +0200 | wenzelm | added NO_CASES; | changeset | files |
| Thu, 18 Aug 2005 11:17:47 +0200 | wenzelm | moved after method.ML; | changeset | files |
| Thu, 18 Aug 2005 11:17:46 +0200 | wenzelm | prepare attributes here; | changeset | files |
| Thu, 18 Aug 2005 11:17:45 +0200 | wenzelm | moved before proof.ML; | changeset | files |
| Thu, 18 Aug 2005 11:17:44 +0200 | wenzelm | added add_locale_context(_i), which returns the body context for presentation; | changeset | files |
| Thu, 18 Aug 2005 11:17:43 +0200 | wenzelm | moved translation functions to Pure/sign.ML; | changeset | files |
| Thu, 18 Aug 2005 11:17:42 +0200 | wenzelm | various Toplevel.theory_context commands: proper presentation in context; | changeset | files |
| Thu, 18 Aug 2005 11:17:41 +0200 | wenzelm | use theory instead of obsolete Sign.sg; | changeset | files |
| 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 |
| Tue, 16 Aug 2005 13:42:48 +0200 | wenzelm | added String.isSuffix; | changeset | files |
| Tue, 16 Aug 2005 13:42:47 +0200 | wenzelm | state: body context; | changeset | files |
| Tue, 16 Aug 2005 13:42:46 +0200 | wenzelm | P.tags; | changeset | files |
| Tue, 16 Aug 2005 13:42:45 +0200 | wenzelm | use_dir: removed hidden, added doc_versions; | changeset | files |
| Tue, 16 Aug 2005 13:42:44 +0200 | wenzelm | back: removed ill-defined '!' option; | changeset | files |
| Tue, 16 Aug 2005 13:42:43 +0200 | wenzelm | added transfer; | changeset | files |
| Tue, 16 Aug 2005 13:42:42 +0200 | wenzelm | moved structure Keyword to OuterKeyword (Isar/outer_keyword.ML); | changeset | files |
| Tue, 16 Aug 2005 13:42:41 +0200 | wenzelm | added tags parser; | changeset | files |
| Tue, 16 Aug 2005 13:42:40 +0200 | wenzelm | clarify is_newline vs. is_blank; | changeset | files |
| Tue, 16 Aug 2005 13:42:39 +0200 | wenzelm | default tags for theory/proof/ML commands; | changeset | files |
| Tue, 16 Aug 2005 13:42:38 +0200 | wenzelm | reimplemented theory presentation, with support for tagged command regions; | changeset | files |
| Tue, 16 Aug 2005 13:42:37 +0200 | wenzelm | back: removed ill-defined '!' option; | changeset | files |
| Tue, 16 Aug 2005 13:42:36 +0200 | wenzelm | replaced sign by thy; | changeset | files |
| Tue, 16 Aug 2005 13:42:35 +0200 | wenzelm | added liberal_name; | changeset | files |
| Tue, 16 Aug 2005 13:42:34 +0200 | wenzelm | tuned Symbol.spaces; | changeset | files |
| Tue, 16 Aug 2005 13:42:33 +0200 | wenzelm | tuned Buffer.add; | changeset | files |
| Tue, 16 Aug 2005 13:42:32 +0200 | wenzelm | tuned unsuffix/unprefix; | changeset | files |
| Tue, 16 Aug 2005 13:42:31 +0200 | wenzelm | type proof: theory_ref instead of theory (make proof contexts independent entities); | changeset | files |
| Tue, 16 Aug 2005 13:42:30 +0200 | wenzelm | Isar command keyword classification (from Isar/outer_syntax.ML); | changeset | files |