| Mon, 26 Nov 2001 17:48:22 +0100 | wenzelm | clarified order in gen_merge_lists'; | changeset | files |
| Sat, 24 Nov 2001 17:21:47 +0100 | wenzelm | fixed SML/NJ error (!?); | changeset | files |
| Sat, 24 Nov 2001 17:02:39 +0100 | wenzelm | use merge_lists, merge_alists; | changeset | files |
| Sat, 24 Nov 2001 17:01:00 +0100 | wenzelm | Symtab.merge_multi'; | changeset | files |
| Sat, 24 Nov 2001 17:00:35 +0100 | wenzelm | type variables: clarified "used" vs. "occ"; | changeset | files |
| Sat, 24 Nov 2001 16:59:44 +0100 | wenzelm | Library.gen_merge_lists'; | changeset | files |
| Sat, 24 Nov 2001 16:59:32 +0100 | wenzelm | clarified locale operations (rename, merge); | changeset | files |
| Sat, 24 Nov 2001 16:58:57 +0100 | wenzelm | print_locale: expr; | changeset | files |
| Sat, 24 Nov 2001 16:58:31 +0100 | wenzelm | added join, merge_multi('); | changeset | files |
| Sat, 24 Nov 2001 16:57:34 +0100 | wenzelm | merge_stamps: merge_lists' with reversed args; | changeset | files |
| Sat, 24 Nov 2001 16:56:26 +0100 | wenzelm | gen_merge_lists; | changeset | files |
| Sat, 24 Nov 2001 16:55:56 +0100 | wenzelm | added gen_merge_lists(') and merge_lists('); | changeset | files |
| Sat, 24 Nov 2001 16:55:00 +0100 | wenzelm | gen_merge_lists'; | changeset | files |
| Sat, 24 Nov 2001 16:54:32 +0100 | wenzelm | generic_merge; | changeset | files |
| Sat, 24 Nov 2001 16:54:10 +0100 | wenzelm | converted simp lemmas; | changeset | files |
| Sat, 24 Nov 2001 16:53:31 +0100 | wenzelm | tuned; | changeset | files |
| Sat, 24 Nov 2001 13:58:19 +0100 | berghofe | Extended match_proof to handle abstractions. | changeset | files |
| Fri, 23 Nov 2001 19:20:58 +0100 | wenzelm | tuned; | changeset | files |
| Fri, 23 Nov 2001 19:20:06 +0100 | wenzelm | improved ordering of evaluated elements; | changeset | files |
| Fri, 23 Nov 2001 19:19:35 +0100 | wenzelm | time_use_thy "Locales"; | changeset | files |
| Fri, 23 Nov 2001 17:19:14 +0100 | nipkow | Isar conversion | changeset | files |
| Thu, 22 Nov 2001 23:46:33 +0100 | wenzelm | theory Locales temporarily disabled; | changeset | files |
| Thu, 22 Nov 2001 23:45:57 +0100 | wenzelm | beginnings of actual locale expressions; | changeset | files |
| Thu, 22 Nov 2001 23:45:23 +0100 | wenzelm | improved locale expression syntax; | changeset | files |
| Thu, 22 Nov 2001 23:44:57 +0100 | wenzelm | locale expression import; | changeset | files |
| Thu, 22 Nov 2001 23:44:30 +0100 | wenzelm | import locale expression; | changeset | files |
| Thu, 22 Nov 2001 23:15:12 +0100 | wenzelm | tuned; | changeset | files |
| Thu, 22 Nov 2001 17:14:17 +0100 | wenzelm | added uname; | changeset | files |
| Thu, 22 Nov 2001 17:13:36 +0100 | wenzelm | tuned; | changeset | files |
| Thu, 22 Nov 2001 17:13:24 +0100 | wenzelm | thm "point.defs"; | changeset | files |
| Thu, 22 Nov 2001 17:13:06 +0100 | wenzelm | recovered original "make"; | changeset | files |
| Thu, 22 Nov 2001 17:12:08 +0100 | wenzelm | renamed "fields" to "flds" (avoid clash with new "fields" operation); | changeset | files |
| Wed, 21 Nov 2001 20:20:18 +0100 | wenzelm | locale expressions; | changeset | files |
| Wed, 21 Nov 2001 00:36:51 +0100 | wenzelm | use tracing function for trace output; | changeset | files |
| Wed, 21 Nov 2001 00:35:13 +0100 | wenzelm | tracing_fn; | changeset | files |
| Wed, 21 Nov 2001 00:34:38 +0100 | wenzelm | added tracing, tracing_fn; | changeset | files |
| Wed, 21 Nov 2001 00:34:06 +0100 | wenzelm | Set.vimage; | changeset | files |
| Wed, 21 Nov 2001 00:33:40 +0100 | wenzelm | got rid of theory Inverse_Image; | changeset | files |
| Wed, 21 Nov 2001 00:33:04 +0100 | wenzelm | theory Inverse_Image converted and moved to Set; | changeset | files |
| Wed, 21 Nov 2001 00:32:10 +0100 | wenzelm | tuned; | changeset | files |
| Tue, 20 Nov 2001 22:54:06 +0100 | wenzelm | tuned; | changeset | files |
| Tue, 20 Nov 2001 22:53:50 +0100 | wenzelm | fixed links etc.; | changeset | files |
| Tue, 20 Nov 2001 22:53:05 +0100 | wenzelm | * HOL/record: cases/induct for more parts; | changeset | files |
| Tue, 20 Nov 2001 20:57:46 +0100 | wenzelm | prefer later trfuns; | changeset | files |
| Tue, 20 Nov 2001 20:57:07 +0100 | wenzelm | moved prefixes1, suffixes1 to library.ML; | changeset | files |
| Tue, 20 Nov 2001 20:56:42 +0100 | wenzelm | trfuns *after* binder syntax; | changeset | files |
| Tue, 20 Nov 2001 20:56:13 +0100 | wenzelm | added prefixes1, suffixes1; | changeset | files |
| Tue, 20 Nov 2001 20:55:50 +0100 | wenzelm | print_depth 10; | changeset | files |
| Tue, 20 Nov 2001 20:55:33 +0100 | wenzelm | derive cases/induct rules for ``more'' parts; | changeset | files |
| Tue, 20 Nov 2001 20:54:12 +0100 | wenzelm | tuned; | changeset | files |
| Tue, 20 Nov 2001 10:48:38 +0100 | paulson | Hyperreal | changeset | files |
| Mon, 19 Nov 2001 23:37:01 +0100 | wenzelm | improved treatment of common result name; | changeset | files |
| Mon, 19 Nov 2001 20:47:57 +0100 | wenzelm | tuned; | changeset | files |
| Mon, 19 Nov 2001 20:47:39 +0100 | wenzelm | multi_theorem: common statement header (covers *all* results); | changeset | files |
| Mon, 19 Nov 2001 20:46:38 +0100 | wenzelm | fixed comment; | changeset | files |
| Mon, 19 Nov 2001 20:46:05 +0100 | wenzelm | induct method: localize rews for rule; | changeset | files |
| Mon, 19 Nov 2001 17:42:00 +0100 | berghofe | Now handles different theorems with same name more gracefully. | changeset | files |
| Mon, 19 Nov 2001 17:40:45 +0100 | berghofe | Improved error message. | changeset | files |
| Mon, 19 Nov 2001 17:40:07 +0100 | berghofe | Added setup. | changeset | files |
| Mon, 19 Nov 2001 17:39:31 +0100 | berghofe | Moved fastype to Envir. | changeset | files |
| Mon, 19 Nov 2001 17:38:09 +0100 | berghofe | Further restructuring of theorem naming functions. | changeset | files |
| Mon, 19 Nov 2001 17:36:40 +0100 | berghofe | Added setup for proof rewrite rules. | changeset | files |
| Mon, 19 Nov 2001 17:36:05 +0100 | berghofe | - Fixed bug in shrink | changeset | files |
| Mon, 19 Nov 2001 17:34:02 +0100 | berghofe | Replaced devar by Envir.head_norm | changeset | files |
| Mon, 19 Nov 2001 17:32:49 +0100 | berghofe | Moved head_norm and fastype from unify.ML to envir.ML | changeset | files |
| Fri, 16 Nov 2001 23:02:58 +0100 | kleing | fixed maxs bug | changeset | files |
| Fri, 16 Nov 2001 22:11:19 +0100 | wenzelm | Ntree and Brouwer converted and moved to ZF/Induct; | changeset | files |
| Fri, 16 Nov 2001 22:10:27 +0100 | wenzelm | converted; | changeset | files |
| Fri, 16 Nov 2001 22:09:44 +0100 | wenzelm | actually store "coinduct" rule; | changeset | files |
| Fri, 16 Nov 2001 22:08:55 +0100 | wenzelm | additional P.marg_comment; | changeset | files |
| Fri, 16 Nov 2001 22:08:28 +0100 | wenzelm | \usepackage[latin1]{inputenc}; | changeset | files |
| Fri, 16 Nov 2001 18:24:11 +0100 | paulson | even more theories from Jacques | changeset | files |
| Fri, 16 Nov 2001 15:25:17 +0100 | wenzelm | finish_global: Drule.strip_shyps_warning (just for warning); | changeset | files |
| Fri, 16 Nov 2001 15:24:39 +0100 | wenzelm | ext_tsig_classes: rebuild_tsig!!!!! | changeset | files |
| Fri, 16 Nov 2001 15:24:09 +0100 | wenzelm | local_standard: plain strip_shyps instead of strip_shyps_warning; | changeset | files |
| Fri, 16 Nov 2001 13:48:43 +0100 | paulson | last-minute tidying | changeset | files |
| Thu, 15 Nov 2001 23:26:58 +0100 | wenzelm | updated; | changeset | files |
| Thu, 15 Nov 2001 23:25:46 +0100 | wenzelm | GPLed; | changeset | files |
| Thu, 15 Nov 2001 23:25:01 +0100 | wenzelm | write_keywords: string argument (logic name); | changeset | files |
| Thu, 15 Nov 2001 23:21:57 +0100 | wenzelm | isatool unsymbolize; | changeset | files |
| Thu, 15 Nov 2001 20:01:19 +0100 | ehmety | Modified to make the files build with the new changes in ZF | changeset | files |
| Thu, 15 Nov 2001 18:37:34 +0100 | wenzelm | depends on Epsilon! | changeset | files |
| Thu, 15 Nov 2001 18:36:24 +0100 | wenzelm | fix_frees: rev; | changeset | files |
| Thu, 15 Nov 2001 18:36:07 +0100 | wenzelm | prove: raise ERROR_MESSAGE; | changeset | files |
| Thu, 15 Nov 2001 18:35:15 +0100 | wenzelm | updated; | changeset | files |
| Thu, 15 Nov 2001 18:34:58 +0100 | wenzelm | * ZF: new-style theory commands '(co)inductive', '(co)datatype', | changeset | files |
| Thu, 15 Nov 2001 18:21:38 +0100 | wenzelm | type_solver_tac: use TCSET' to refer to context of goal state (does | changeset | files |
| Thu, 15 Nov 2001 18:20:48 +0100 | wenzelm | setup DatatypeTactics.setup; | changeset | files |
| Thu, 15 Nov 2001 18:20:13 +0100 | wenzelm | added Induct/Binary_Trees.thy, Induct/Tree_Forest (converted from | changeset | files |
| Thu, 15 Nov 2001 18:18:17 +0100 | wenzelm | no handle ERROR; | changeset | files |
| Thu, 15 Nov 2001 18:16:17 +0100 | wenzelm | fixed; | changeset | files |
| Thu, 15 Nov 2001 18:15:58 +0100 | wenzelm | Isar version of 'rep_datatype'; | changeset | files |
| Thu, 15 Nov 2001 18:15:32 +0100 | wenzelm | avoid handle _; | changeset | files |
| Thu, 15 Nov 2001 18:15:13 +0100 | wenzelm | added TCSET(') tacticals; | changeset | files |
| Thu, 15 Nov 2001 18:09:40 +0100 | wenzelm | added Term and Tree_Forest (from converted ZF/ex); | changeset | files |
| Thu, 15 Nov 2001 18:08:19 +0100 | wenzelm | TF and Term moved to ZF/Induct; | changeset | files |
| Thu, 15 Nov 2001 17:59:56 +0100 | paulson | miniscoping of UN and INT | changeset | files |
| Thu, 15 Nov 2001 16:48:05 +0100 | ehmety | Added new entry | changeset | files |
| Thu, 15 Nov 2001 16:46:38 +0100 | ehmety | New files | changeset | files |
| Thu, 15 Nov 2001 16:12:49 +0100 | paulson | new theories from Jacques Fleuriot | changeset | files |
| Thu, 15 Nov 2001 15:07:16 +0100 | ehmety | *** empty log message *** | changeset | files |
| Wed, 14 Nov 2001 23:22:43 +0100 | wenzelm | converted datatype examples moved from ZF/ex to ZF/Induct; | changeset | files |
| Wed, 14 Nov 2001 23:22:15 +0100 | wenzelm | document setup; | changeset | files |
| Wed, 14 Nov 2001 23:21:05 +0100 | wenzelm | removed BT, Data, Enum (see ZF/Induct); | changeset | files |
| Wed, 14 Nov 2001 23:20:41 +0100 | wenzelm | case_names; | changeset | files |
| Wed, 14 Nov 2001 23:20:14 +0100 | wenzelm | added Datatypes, Binary_Trees (from ZF/ex); | changeset | files |
| Wed, 14 Nov 2001 23:19:09 +0100 | wenzelm | Isar attribute and method setup; | changeset | files |
| Wed, 14 Nov 2001 23:18:37 +0100 | wenzelm | fix path prefix; | changeset | files |
| Wed, 14 Nov 2001 23:18:13 +0100 | wenzelm | use proper intr_names (for required case_names); | changeset | files |
| Wed, 14 Nov 2001 23:16:05 +0100 | wenzelm | added Induct/Binary_Trees.thy, Induct/Datatypes.thy; | changeset | files |
| Wed, 14 Nov 2001 23:15:19 +0100 | wenzelm | tuned; | changeset | files |
| Wed, 14 Nov 2001 23:14:59 +0100 | wenzelm | updated; | changeset | files |
| Wed, 14 Nov 2001 18:46:30 +0100 | wenzelm | adapted primrec/datatype to Isar; | changeset | files |
| Wed, 14 Nov 2001 18:46:07 +0100 | wenzelm | tuned; | changeset | files |
| Wed, 14 Nov 2001 18:45:38 +0100 | wenzelm | store original simps for codegen; | changeset | files |
| Wed, 14 Nov 2001 18:44:27 +0100 | wenzelm | inductive: removed con_defs; | changeset | files |
| Wed, 14 Nov 2001 18:42:34 +0100 | wenzelm | updated; | changeset | files |
| Tue, 13 Nov 2001 22:36:38 +0100 | wenzelm | updated; | changeset | files |
| Tue, 13 Nov 2001 22:25:59 +0100 | wenzelm | * ZF: new-style theory commands 'inductive', 'inductive_cases', and | changeset | files |
| Tue, 13 Nov 2001 22:24:28 +0100 | wenzelm | ZF specific keywords; | changeset | files |