| 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 |
| 2001-11-28 |
wenzelm |
2001-11-28 |
variant: preserve suffix of underscores (for skolem/internal names etc.);
|
file | diff | annotate |
| 2001-10-24 |
wenzelm |
2001-10-24 |
added lambda;
|
file | diff | annotate |
| 2001-10-23 |
wenzelm |
2001-10-23 |
replace_dummy_patterns: lift over bounds;
|
file | diff | annotate |
| 2001-05-31 |
wenzelm |
2001-05-31 |
invent_names
|
file | diff | annotate |
| 2001-01-06 |
wenzelm |
2001-01-06 |
added list_abs;
|
file | diff | annotate |
| 2000-12-13 |
wenzelm |
2000-12-13 |
fixed add_term_names: NameSpace.base;
|
file | diff | annotate |
| 2000-11-30 |
wenzelm |
2000-11-30 |
added is_replaced_dummy_pattern;
|
file | diff | annotate |
| 2000-08-29 |
nipkow |
2000-08-29 |
*** empty log message ***
|
file | diff | annotate |
| 2000-08-04 |
wenzelm |
2000-08-04 |
added dummy_patternN, no_dummy_patterns, replace_dummy_patterns;
|
file | diff | annotate |
| 2000-07-13 |
wenzelm |
2000-07-13 |
add_term_consts: ins_string;
|
file | diff | annotate |
| 2000-03-30 |
wenzelm |
2000-03-30 |
foldl_term_types: depend on term as well;
|
file | diff | annotate |
| 2000-03-10 |
berghofe |
2000-03-10 |
Added functions subst_TVars_Vartab and typ_subst_TVars_Vartab.
|
file | diff | annotate |
| 1999-09-29 |
wenzelm |
1999-09-29 |
added rems_sort;
|
file | diff | annotate |
| 1999-09-01 |
wenzelm |
1999-09-01 |
structure Termtab;
|
file | diff | annotate |
| 1999-08-23 |
nipkow |
1999-08-23 |
Corrected two busg in the simplifier.
|
file | diff | annotate |
| 1999-07-10 |
wenzelm |
1999-07-10 |
Symtab.lookup_multi;
|
file | diff | annotate |
| 1999-04-30 |
wenzelm |
1999-04-30 |
val foldl_map_aterms: ('a * term -> 'a * term) -> 'a * term -> 'a * term;
|
file | diff | annotate |
| 1998-12-18 |
paulson |
1998-12-18 |
moved dest_Type to term.ML from HOL/Tools/primrec_package
|
file | diff | annotate |
| 1998-11-29 |
wenzelm |
1998-11-29 |
added oct_char;
|
file | diff | annotate |
| 1998-09-29 |
paulson |
1998-09-29 |
new function inter_term
|
file | diff | annotate |
| 1998-03-09 |
wenzelm |
1998-03-09 |
tuned some names;
|
file | diff | annotate |
| 1998-02-18 |
nipkow |
1998-02-18 |
Improved loop-test for rewrite rules a little.
Should be done properly!
|
file | diff | annotate |
| 1998-02-12 |
wenzelm |
1998-02-12 |
tuned comments;
|
file | diff | annotate |
| 1998-02-06 |
wenzelm |
1998-02-06 |
added Vartab: TABLE;
|
file | diff | annotate |
| 1997-12-28 |
wenzelm |
1997-12-28 |
made MLWorks happy;
|
file | diff | annotate |
| 1997-12-28 |
wenzelm |
1997-12-28 |
renamed Symtab.null to Symtab.empty;
|
file | diff | annotate |
| 1997-12-24 |
wenzelm |
1997-12-24 |
export range_type;
|
file | diff | annotate |
| 1997-12-22 |
paulson |
1997-12-22 |
Added range-type for completeness
|
file | diff | annotate |
| 1997-12-19 |
wenzelm |
1997-12-19 |
term order;
signature;
|
file | diff | annotate |
| 1997-11-26 |
wenzelm |
1997-11-26 |
added foldl_atyps: ('a * typ -> 'a) -> 'a * typ -> 'a;
added foldl_aterms: ('a * term -> 'a) -> 'a * term -> 'a;
added foldl_types: ('a * typ -> 'a) -> 'a * term -> 'a;
|
file | diff | annotate |
| 1997-11-07 |
oheimb |
1997-11-07 |
changed libraray function find to find_index_eq, currying it
|
file | diff | annotate |
| 1997-11-07 |
oheimb |
1997-11-07 |
added exists_Const
|
file | diff | annotate |
| 1997-11-01 |
paulson |
1997-11-01 |
New syntax function for types
|
file | diff | annotate |
| 1997-10-28 |
wenzelm |
1997-10-28 |
add_typ_classes, add_typ_tycons, add_term_classes, add_term_tycons,
add_term_consts, map_typ, map_term: moved from sign.ML to term.ML;
|
file | diff | annotate |