| Mon, 06 Feb 2006 20:59:50 +0100 | wenzelm | cert_def: use Logic.dest_def; | changeset | files |
| Mon, 06 Feb 2006 20:59:49 +0100 | wenzelm | Toplevel.local_theory; | changeset | files |
| Mon, 06 Feb 2006 20:59:48 +0100 | wenzelm | LocalDefs.cert_def; | changeset | files |
| Mon, 06 Feb 2006 20:59:47 +0100 | wenzelm | eq_prop: Envir.beta_eta_contract; | changeset | files |
| Mon, 06 Feb 2006 20:59:46 +0100 | wenzelm | renamed xxx_multi to xxx_list; | changeset | files |
| Mon, 06 Feb 2006 20:59:42 +0100 | wenzelm | moved combound, rlist_abs to logic.ML; | changeset | files |
| Mon, 06 Feb 2006 20:59:11 +0100 | wenzelm | union_tpairs: Library.merge; | changeset | files |
| Mon, 06 Feb 2006 20:59:10 +0100 | wenzelm | moved no_vars to sign.ML; | changeset | files |
| Mon, 06 Feb 2006 20:59:09 +0100 | wenzelm | lambda: abstract over any const; | changeset | files |
| Mon, 06 Feb 2006 20:59:08 +0100 | wenzelm | added add_abbrevs(_i); | changeset | files |
| Mon, 06 Feb 2006 20:59:07 +0100 | wenzelm | moved (beta_)eta_contract to envir.ML; | changeset | files |
| Mon, 06 Feb 2006 20:59:06 +0100 | wenzelm | tuned; | changeset | files |
| Mon, 06 Feb 2006 20:59:05 +0100 | wenzelm | added generic dest_def (mostly from theory.ML); | changeset | files |
| Mon, 06 Feb 2006 20:59:04 +0100 | wenzelm | added (beta_)eta_contract (from pattern.ML); | changeset | files |
| Mon, 06 Feb 2006 20:59:03 +0100 | wenzelm | print_theory: const abbreviations; | changeset | files |
| Mon, 06 Feb 2006 20:59:02 +0100 | wenzelm | added abbreviations; | changeset | files |
| Mon, 06 Feb 2006 20:59:01 +0100 | wenzelm | load envir.ML and logic.ML early; | changeset | files |
| Mon, 06 Feb 2006 20:59:00 +0100 | wenzelm | Logic.rlist_abs; | changeset | files |
| Mon, 06 Feb 2006 20:58:59 +0100 | wenzelm | Logic.const_of_class/class_of_const; | changeset | files |
| Mon, 06 Feb 2006 20:58:57 +0100 | wenzelm | TableFun: renamed xxx_multi to xxx_list; | changeset | files |
| Mon, 06 Feb 2006 20:58:56 +0100 | wenzelm | replaced Symtab.merge_multi by local merge_rules; | changeset | files |
| Mon, 06 Feb 2006 20:58:54 +0100 | wenzelm | Envir.(beta_)eta_contract; | changeset | files |
| Mon, 06 Feb 2006 11:01:28 +0100 | haftmann | subsituted gen_duplicates / has_duplicates for duplicates whenever appropriate | changeset | files |
| Mon, 06 Feb 2006 11:00:24 +0100 | haftmann | added strip_abs | changeset | files |
| Mon, 06 Feb 2006 11:00:06 +0100 | haftmann | clarified semantics of merge | changeset | files |
| Sat, 04 Feb 2006 03:14:32 +0100 | huffman | speedup: use simproc for AC rules | changeset | files |
| Sat, 04 Feb 2006 02:37:09 +0100 | huffman | UU_reorient_simproc no longer rewrites UU = numeral | changeset | files |
| Fri, 03 Feb 2006 23:12:31 +0100 | wenzelm | removed obsolete gen_ins/mem; | changeset | files |
| Fri, 03 Feb 2006 23:12:30 +0100 | wenzelm | removed add/del_rules; | changeset | files |
| Fri, 03 Feb 2006 23:12:28 +0100 | wenzelm | canonical member/insert/merge; | changeset | files |
| Fri, 03 Feb 2006 17:08:03 +0100 | paulson | removal of case analysis clauses | changeset | files |
| Fri, 03 Feb 2006 17:02:33 +0100 | haftmann | fix | changeset | files |
| Fri, 03 Feb 2006 11:48:11 +0100 | haftmann | minor improvements | changeset | files |
| Fri, 03 Feb 2006 11:47:57 +0100 | haftmann | refined signature of locale module | changeset | files |
| Fri, 03 Feb 2006 08:48:33 +0100 | haftmann | no toplevel 'thy' anymore | changeset | files |
| Fri, 03 Feb 2006 08:48:16 +0100 | haftmann | fix in codegen | changeset | files |
| Thu, 02 Feb 2006 21:59:55 +0100 | wenzelm | do not open structure; | changeset | files |
| Thu, 02 Feb 2006 19:57:13 +0100 | huffman | reimplemented using Equiv_Relations.thy | changeset | files |
| Thu, 02 Feb 2006 18:04:10 +0100 | haftmann | improvement in devarifications | changeset | files |
| Thu, 02 Feb 2006 18:03:35 +0100 | haftmann | alternative syntax for instances | changeset | files |
| Thu, 02 Feb 2006 16:37:10 +0100 | wenzelm | tuned; | changeset | files |
| Thu, 02 Feb 2006 16:31:38 +0100 | wenzelm | consumes: negative argument relative to total number of prems; | changeset | files |
| Thu, 02 Feb 2006 16:31:37 +0100 | wenzelm | added refine_insert; | changeset | files |
| Thu, 02 Feb 2006 16:31:35 +0100 | wenzelm | Proof.refine_insert; | changeset | files |
| Thu, 02 Feb 2006 16:31:34 +0100 | wenzelm | always use Attrib.src; | changeset | files |
| Thu, 02 Feb 2006 16:31:33 +0100 | wenzelm | more generic type for map_specs/facts; | changeset | files |
| Thu, 02 Feb 2006 16:31:32 +0100 | wenzelm | 'obtains' element; | changeset | files |
| Thu, 02 Feb 2006 16:31:31 +0100 | wenzelm | 'obtain': optional case name; | changeset | files |
| Thu, 02 Feb 2006 16:31:30 +0100 | wenzelm | index elements; | changeset | files |
| Thu, 02 Feb 2006 16:31:28 +0100 | wenzelm | * Isar: 'obtains' element; | changeset | files |
| Thu, 02 Feb 2006 12:54:24 +0100 | wenzelm | tuned msg; | changeset | files |
| Thu, 02 Feb 2006 12:54:08 +0100 | wenzelm | theorem(_in_locale): Element.statement, Obtain.statement; | changeset | files |
| Thu, 02 Feb 2006 12:52:25 +0100 | wenzelm | added parname; | changeset | files |
| Thu, 02 Feb 2006 12:52:24 +0100 | wenzelm | obtain(_i): optional name for 'that'; | changeset | files |
| Thu, 02 Feb 2006 12:52:21 +0100 | wenzelm | tuned comments; | changeset | files |
| Thu, 02 Feb 2006 12:52:20 +0100 | wenzelm | moved (general_)statement to outer_parse.ML; | changeset | files |
| Thu, 02 Feb 2006 12:52:19 +0100 | wenzelm | added concluding statements: Shows/Obtains; | changeset | files |
| Thu, 02 Feb 2006 12:52:18 +0100 | wenzelm | moved specific map_typ/term to sign.ML; | changeset | files |
| Thu, 02 Feb 2006 12:52:16 +0100 | wenzelm | added specific map_typ/term (from term.ML); | changeset | files |
| Thu, 02 Feb 2006 10:24:06 +0100 | krauss | Exporting recdef's hints for use by new recdef package | changeset | files |