| 2006-02-07 |
wenzelm |
lambda: base name of Const;
|
changeset |
files
|
| 2006-02-07 |
wenzelm |
adapted Sign.infer_types;
|
changeset |
files
|
| 2006-02-07 |
wenzelm |
has_duplicates;
|
changeset |
files
|
| 2006-02-07 |
wenzelm |
adapted Sign.infer_types;
|
changeset |
files
|
| 2006-02-07 |
wenzelm |
added local consts component;
|
changeset |
files
|
| 2006-02-07 |
wenzelm |
Library.is_equal;
|
changeset |
files
|
| 2006-02-07 |
wenzelm |
removed obsolete sign_of_cterm;
|
changeset |
files
|
| 2006-02-07 |
wenzelm |
adapted Sign.infer_types(_simult), Sign.certify_term/prop;
|
changeset |
files
|
| 2006-02-07 |
wenzelm |
export consts_of;
|
changeset |
files
|
| 2006-02-07 |
wenzelm |
removed eq-polymorphic duplicates;
|
changeset |
files
|
| 2006-02-07 |
wenzelm |
renamed space to space_of;
|
changeset |
files
|
| 2006-02-07 |
wenzelm |
renamed gen_duplicates to duplicates;
|
changeset |
files
|
| 2006-02-07 |
haftmann |
slight improvements in code generation
|
changeset |
files
|
| 2006-02-06 |
wenzelm |
updated;
|
changeset |
files
|
| 2006-02-06 |
wenzelm |
Logic.combound;
|
changeset |
files
|
| 2006-02-06 |
wenzelm |
adapted Consts.dest;
|
changeset |
files
|
| 2006-02-06 |
wenzelm |
Sign.cert_def;
|
changeset |
files
|
| 2006-02-06 |
wenzelm |
added bound_vars;
|
changeset |
files
|
| 2006-02-06 |
wenzelm |
TableFun: renamed xxx_multi to xxx_list;
|
changeset |
files
|
| 2006-02-06 |
wenzelm |
Envir.(beta_)eta_contract;
|
changeset |
files
|
| 2006-02-06 |
wenzelm |
added local_theory, with optional locale xname;
|
changeset |
files
|
| 2006-02-06 |
wenzelm |
type local_theory;
|
changeset |
files
|
| 2006-02-06 |
wenzelm |
norm_term: Sign.const_expansion, Envir.expand_atom;
|
changeset |
files
|
| 2006-02-06 |
wenzelm |
TableFun: renamed xxx_multi to xxx_list;
|
changeset |
files
|
| 2006-02-06 |
wenzelm |
type local_theory = Proof.context;
|
changeset |
files
|
| 2006-02-06 |
wenzelm |
cert_def: use Logic.dest_def;
|
changeset |
files
|
| 2006-02-06 |
wenzelm |
Toplevel.local_theory;
|
changeset |
files
|
| 2006-02-06 |
wenzelm |
LocalDefs.cert_def;
|
changeset |
files
|
| 2006-02-06 |
wenzelm |
eq_prop: Envir.beta_eta_contract;
|
changeset |
files
|
| 2006-02-06 |
wenzelm |
renamed xxx_multi to xxx_list;
|
changeset |
files
|
| 2006-02-06 |
wenzelm |
moved combound, rlist_abs to logic.ML;
|
changeset |
files
|
| 2006-02-06 |
wenzelm |
union_tpairs: Library.merge;
|
changeset |
files
|
| 2006-02-06 |
wenzelm |
moved no_vars to sign.ML;
|
changeset |
files
|
| 2006-02-06 |
wenzelm |
lambda: abstract over any const;
|
changeset |
files
|
| 2006-02-06 |
wenzelm |
added add_abbrevs(_i);
|
changeset |
files
|
| 2006-02-06 |
wenzelm |
moved (beta_)eta_contract to envir.ML;
|
changeset |
files
|
| 2006-02-06 |
wenzelm |
tuned;
|
changeset |
files
|
| 2006-02-06 |
wenzelm |
added generic dest_def (mostly from theory.ML);
|
changeset |
files
|
| 2006-02-06 |
wenzelm |
added (beta_)eta_contract (from pattern.ML);
|
changeset |
files
|
| 2006-02-06 |
wenzelm |
print_theory: const abbreviations;
|
changeset |
files
|
| 2006-02-06 |
wenzelm |
added abbreviations;
|
changeset |
files
|
| 2006-02-06 |
wenzelm |
load envir.ML and logic.ML early;
|
changeset |
files
|
| 2006-02-06 |
wenzelm |
Logic.rlist_abs;
|
changeset |
files
|
| 2006-02-06 |
wenzelm |
Logic.const_of_class/class_of_const;
|
changeset |
files
|
| 2006-02-06 |
wenzelm |
TableFun: renamed xxx_multi to xxx_list;
|
changeset |
files
|
| 2006-02-06 |
wenzelm |
replaced Symtab.merge_multi by local merge_rules;
|
changeset |
files
|
| 2006-02-06 |
wenzelm |
Envir.(beta_)eta_contract;
|
changeset |
files
|
| 2006-02-06 |
haftmann |
subsituted gen_duplicates / has_duplicates for duplicates whenever appropriate
|
changeset |
files
|
| 2006-02-06 |
haftmann |
added strip_abs
|
changeset |
files
|
| 2006-02-06 |
haftmann |
clarified semantics of merge
|
changeset |
files
|
| 2006-02-04 |
huffman |
speedup: use simproc for AC rules
|
changeset |
files
|
| 2006-02-04 |
huffman |
UU_reorient_simproc no longer rewrites UU = numeral
|
changeset |
files
|
| 2006-02-03 |
wenzelm |
removed obsolete gen_ins/mem;
|
changeset |
files
|
| 2006-02-03 |
wenzelm |
removed add/del_rules;
|
changeset |
files
|
| 2006-02-03 |
wenzelm |
canonical member/insert/merge;
|
changeset |
files
|
| 2006-02-03 |
paulson |
removal of case analysis clauses
|
changeset |
files
|
| 2006-02-03 |
haftmann |
fix
|
changeset |
files
|
| 2006-02-03 |
haftmann |
minor improvements
|
changeset |
files
|
| 2006-02-03 |
haftmann |
refined signature of locale module
|
changeset |
files
|
| 2006-02-03 |
haftmann |
no toplevel 'thy' anymore
|
changeset |
files
|