| Mon, 06 Feb 2006 20:59:52 +0100 |
wenzelm |
TableFun: renamed xxx_multi to xxx_list;
|
changeset |
files
|
| Mon, 06 Feb 2006 20:59:51 +0100 |
wenzelm |
type local_theory = Proof.context;
|
changeset |
files
|
| 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
|