| Fri, 30 Nov 2001 12:18:14 +0100 | paulson | minor tweaks | changeset | files |
| Thu, 29 Nov 2001 21:12:37 +0100 | nipkow | *** empty log message *** | changeset | files |
| Thu, 29 Nov 2001 20:02:23 +0100 | nipkow | *** empty log message *** | changeset | files |
| Thu, 29 Nov 2001 19:03:03 +0100 | nipkow | *** empty log message *** | changeset | files |
| Thu, 29 Nov 2001 17:39:23 +0100 | paulson | minor textual tweaks | changeset | files |
| Thu, 29 Nov 2001 14:12:42 +0100 | nipkow | *** empty log message *** | changeset | files |
| Thu, 29 Nov 2001 13:33:45 +0100 | nipkow | *** empty log message *** | changeset | files |
| Thu, 29 Nov 2001 01:51:38 +0100 | wenzelm | export primitive netpairs; | changeset | files |
| Thu, 29 Nov 2001 01:51:06 +0100 | wenzelm | RuleContext.intro_query_local; | changeset | files |
| Thu, 29 Nov 2001 01:50:50 +0100 | wenzelm | rule context and attributes moved to rule_context.ML; | changeset | files |
| Thu, 29 Nov 2001 01:50:19 +0100 | wenzelm | qualify_elem: do not qualify empty names (""); | changeset | files |
| Thu, 29 Nov 2001 01:49:44 +0100 | wenzelm | tuned; | changeset | files |
| Thu, 29 Nov 2001 00:45:12 +0100 | wenzelm | added deletion of rules; | changeset | files |
| Thu, 29 Nov 2001 00:44:34 +0100 | wenzelm | general type of delete_tagged_brl; | changeset | files |
| Thu, 29 Nov 2001 00:43:39 +0100 | wenzelm | most general type of delete/delete_term; | changeset | files |
| Wed, 28 Nov 2001 23:31:47 +0100 | wenzelm | skip_proof: do not require quick_and_dirty in interactive mode; | changeset | files |
| Wed, 28 Nov 2001 23:30:59 +0100 | wenzelm | support "_::foo" sort constraints; | changeset | files |
| Wed, 28 Nov 2001 23:30:24 +0100 | wenzelm | removed unused simple_read_typ; | changeset | files |
| Wed, 28 Nov 2001 23:29:48 +0100 | wenzelm | added proof_to_theory'; | changeset | files |
| Wed, 28 Nov 2001 23:29:21 +0100 | wenzelm | Syntax.typ_of_term: pass intern sort fn; | changeset | files |
| Wed, 28 Nov 2001 23:28:58 +0100 | wenzelm | Syntax.read_typ: pass intern sort fn; | changeset | files |
| Wed, 28 Nov 2001 23:27:35 +0100 | wenzelm | * Isar/Pure: "sorry" no longer requires quick_and_dirty in interactive mode; | changeset | files |
| Wed, 28 Nov 2001 00:46:26 +0100 | wenzelm | theory data: removed obsolete finish method; | changeset | files |
| Wed, 28 Nov 2001 00:44:37 +0100 | wenzelm | data: removed obsolete finish method; | changeset | files |
| Wed, 28 Nov 2001 00:43:50 +0100 | wenzelm | name space for local thms (export cond_extern, qualified); | changeset | files |
| Wed, 28 Nov 2001 00:42:35 +0100 | wenzelm | print_state: up to 7 result names; | changeset | files |
| Wed, 28 Nov 2001 00:42:04 +0100 | wenzelm | qualify imported facts; | changeset | files |
| Wed, 28 Nov 2001 00:39:33 +0100 | wenzelm | variant: preserve suffix of underscores (for skolem/internal names etc.); | changeset | files |
| Wed, 28 Nov 2001 00:38:11 +0100 | wenzelm | join_rules RuleCases.save; | changeset | files |
| Wed, 28 Nov 2001 00:37:40 +0100 | wenzelm | tuned declarations; | changeset | files |
| Wed, 28 Nov 2001 00:37:08 +0100 | wenzelm | tuned; | changeset | files |
| Tue, 27 Nov 2001 13:28:26 +0100 | wenzelm | make SML/NJ happy; | changeset | files |
| Mon, 26 Nov 2001 23:24:27 +0100 | wenzelm | added Pure/Isar/rule_context.ML; | changeset | files |
| Mon, 26 Nov 2001 23:23:33 +0100 | wenzelm | gcd_dvd1 and gcd_dvd2 proven simultaneously; | changeset | files |
| Mon, 26 Nov 2001 18:34:17 +0100 | wenzelm | moved lemmas to theory Hilbert_Choice; | changeset | files |
| Mon, 26 Nov 2001 18:33:57 +0100 | wenzelm | tuned; | changeset | files |
| Mon, 26 Nov 2001 18:33:21 +0100 | wenzelm | added remdups_rl; | changeset | files |
| Mon, 26 Nov 2001 18:33:08 +0100 | wenzelm | clarified order of merge_lists'; | changeset | files |
| 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 |