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
|