| 2006-01-31 |
wenzelm |
2006-01-31 |
lambda: abstract over TYPE argument, too;
|
file | diff | annotate |
| 2006-01-30 |
haftmann |
2006-01-30 |
added map_atype, map_aterms
|
file | diff | annotate |
| 2005-11-25 |
wenzelm |
2005-11-25 |
added dummy_pattern;
|
file | diff | annotate |
| 2005-11-16 |
wenzelm |
2005-11-16 |
added betapplys;
|
file | diff | annotate |
| 2005-11-10 |
wenzelm |
2005-11-10 |
added find_free (from Isar/proof_context.ML);
|
file | diff | annotate |
| 2005-11-09 |
wenzelm |
2005-11-09 |
removed obsolete term set operations;
|
file | diff | annotate |
| 2005-10-15 |
wenzelm |
2005-10-15 |
tuned comments;
|
file | diff | annotate |
| 2005-10-07 |
wenzelm |
2005-10-07 |
added absdummy;
|
file | diff | annotate |
| 2005-10-07 |
wenzelm |
2005-10-07 |
added str_of_term (from HOL/Tools/ATP/recon_translate_proof.ML);
|
file | diff | annotate |
| 2005-10-04 |
wenzelm |
2005-10-04 |
minor tweaks for Poplog/ML;
|
file | diff | annotate |
| 2005-09-25 |
wenzelm |
2005-09-25 |
zero_var_inst: replace loose bounds :000 etc.;
|
file | diff | annotate |
| 2005-09-08 |
haftmann |
2005-09-08 |
introduces some modern-style AList operations
|
file | diff | annotate |
| 2005-09-06 |
haftmann |
2005-09-06 |
introduced some new-style AList operations
|
file | diff | annotate |
| 2005-08-01 |
wenzelm |
2005-08-01 |
removed atless (use term_ord instead);
removed (inefficient) insert_aterm;
improved bound: nameless, avoid allocating new strings;
tuned sort_ord/typ_ord: dict_ord;
tuned abstract_over: SAME;
tuned add_term_vars/frees: OrdList.insert;
removed compress_type/compress_type (cf. compress.ML);
|
file | diff | annotate |
| 2005-07-28 |
wenzelm |
2005-07-28 |
added add_tfreesT, add_tfrees;
added bound;
added zero_var_indexesT, zero_var_indexes, zero_var_indexes_subst;
removed add_term_constsT;
tuned;
|
file | diff | annotate |
| 2005-07-19 |
wenzelm |
2005-07-19 |
moved incr_tvar to logic.ML;
added eq_var, eq_tvar, instantiate, instantiateT;
|
file | diff | annotate |
| 2005-07-15 |
wenzelm |
2005-07-15 |
replaced foldl_XXX by canonical fold_XXX;
canonical arguments for add_term_varnames, add_tvarsT, add_tvars, add_vars, add_frees,
|
file | diff | annotate |
| 2005-07-13 |
wenzelm |
2005-07-13 |
fixed comment-out;
|
file | diff | annotate |
| 2005-07-13 |
haftmann |
2005-07-13 |
(fix for an accidental commit)
|
file | diff | annotate |
| 2005-07-13 |
haftmann |
2005-07-13 |
(intermediate commit)
|
file | diff | annotate |
| 2005-07-06 |
wenzelm |
2005-07-06 |
tuned eq_ix;
|
file | diff | annotate |
| 2005-07-06 |
wenzelm |
2005-07-06 |
tuned maxidx_of_typ/typs/term;
moved adhoc string_of_term to HOL/Tools/ATP/recon_translate_proof.ML;
cleaned signature;
|
file | diff | annotate |
| 2005-07-04 |
wenzelm |
2005-07-04 |
added fast_indexname_ord, fast_term_ord;
changed sort_ord, typ_ord, Vartab, Termtab: use fast orders;
added argument_type_of, dest_abs;
tuned;
|
file | diff | annotate |
| 2005-07-01 |
wenzelm |
2005-07-01 |
tuned term_ord: less garbage;
|
file | diff | annotate |
| 2005-06-29 |
wenzelm |
2005-06-29 |
tuned sort_ord: pointer_eq;
tuned size_of_term: less stack usage;
|
file | diff | annotate |
| 2005-06-28 |
paulson |
2005-06-28 |
first-order check now allows quantifiers
|
file | diff | annotate |
| 2005-06-25 |
nipkow |
2005-06-25 |
Added term_lpo
|
file | diff | annotate |
| 2005-06-22 |
wenzelm |
2005-06-22 |
export sort_ord;
tuned term_ord, typ_ord: use pointer_eq;
tuned aconv, aconvs: based on term_ord;
|
file | diff | annotate |
| 2005-06-09 |
wenzelm |
2005-06-09 |
map_typ and map_term no longer global;
|
file | diff | annotate |
| 2005-06-06 |
wenzelm |
2005-06-06 |
avoid polymorphic ins;
|
file | diff | annotate |
| 2005-05-29 |
obua |
2005-05-29 |
Implement cycle-free overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
|
file | diff | annotate |
| 2005-05-22 |
wenzelm |
2005-05-22 |
added show_dummy_patterns;
|
file | diff | annotate |
| 2005-05-17 |
wenzelm |
2005-05-17 |
renamed show_var_qmarks to show_question_marks;
string_of_vname: improved treatment of \<^isub> and \<^isup>;
|
file | diff | annotate |
| 2005-05-16 |
kleing |
2005-05-16 |
line wrap
|
file | diff | annotate |
| 2005-05-12 |
paulson |
2005-05-12 |
first-order now ignores "all"
|
file | diff | annotate |
| 2005-05-03 |
dixon |
2005-05-03 |
lucas - added dest_TVar and dest_TFree.
|
file | diff | annotate |
| 2005-04-21 |
berghofe |
2005-04-21 |
- Eliminated nodup_vars check.
- Unification and matching functions now check types of term variables / sorts
of type variables when applying a substitution.
- Thm.instantiate now takes (ctyp * ctyp) list instead of (indexname * ctyp) list
as argument, to allow for proper instantiation of theorems containing
type variables with same name but different sorts.
|
file | diff | annotate |
| 2005-03-26 |
gagern |
2005-03-26 |
op vor infix-Konstruktoren im datatype binding zum besseren Parsen
|
file | diff | annotate |
| 2005-03-17 |
nipkow |
2005-03-17 |
added string_of_term
|
file | diff | annotate |
| 2005-03-10 |
ballarin |
2005-03-10 |
Registrations of global locale interpretations: improved, better naming.
|
file | diff | annotate |
| 2005-03-04 |
skalberg |
2005-03-04 |
Removed practically all references to Library.foldr.
|
file | diff | annotate |
| 2005-03-04 |
paulson |
2005-03-04 |
new first_order test
|
file | diff | annotate |
| 2005-03-03 |
skalberg |
2005-03-03 |
Move towards standard functions.
|
file | diff | annotate |
| 2005-02-13 |
skalberg |
2005-02-13 |
Deleted Library.option type.
|
file | diff | annotate |
| 2005-01-27 |
berghofe |
2005-01-27 |
Added show_var_qmarks flag.
|
file | diff | annotate |
| 2004-07-08 |
wenzelm |
2004-07-08 |
added add_term_varnames, term_varnames;
|
file | diff | annotate |
| 2004-06-01 |
wenzelm |
2004-06-01 |
removed obsolete sort 'logic';
|
file | diff | annotate |
| 2004-05-29 |
wenzelm |
2004-05-29 |
moved read_int etc. to library.ML; added type 'arity';
|
file | diff | annotate |
| 2004-05-21 |
wenzelm |
2004-05-21 |
moved some sort ops to sorts.ML; added string_of_vname (from Syntax module);
|
file | diff | annotate |
| 2004-05-01 |
wenzelm |
2004-05-01 |
improved Term.invent_names;
|
file | diff | annotate |
| 2004-04-26 |
wenzelm |
2004-04-26 |
variant: use Symbol.bump_init;
|
file | diff | annotate |
| 2004-03-19 |
paulson |
2004-03-19 |
Removing the datatype declaration of "order" allows the standard General.order
to be used. Thus we can use Int.compare and String.compare instead of the
slower home-grown versions.
|
file | diff | annotate |
| 2002-10-21 |
berghofe |
2002-10-21 |
- removed flexpair
- added maxidx_of_terms
- tuned lambda: now also abstracts over Vars
|
file | diff | annotate |
| 2002-10-14 |
nipkow |
2002-10-14 |
Ported find_intro/elim to Isar.
|
file | diff | annotate |
| 2002-08-08 |
wenzelm |
2002-08-08 |
adhoc_freeze_vars;
|
file | diff | annotate |
| 2002-03-01 |
wenzelm |
2002-03-01 |
structure Typtab;
clarified typ_ord;
clarified compress_type;
|
file | diff | annotate |
| 2002-02-28 |
wenzelm |
2002-02-28 |
added match_bvars, rename_abs (from thm.ML);
|
file | diff | annotate |
| 2002-02-20 |
wenzelm |
2002-02-20 |
Symbol.bump_string;
|
file | diff | annotate |
| 2002-01-17 |
wenzelm |
2002-01-17 |
added add_term_free_names (more precise/efficient than add_term_names);
|
file | diff | annotate |
| 2001-12-14 |
wenzelm |
2001-12-14 |
added invent_type_names;
added add_tvarsT etc. (from drule.ML);
|
file | diff | annotate |