| Fri, 01 Mar 2002 22:30:01 +0100 |
wenzelm |
structure Typtab;
|
file |
diff |
annotate
|
| Thu, 28 Feb 2002 19:23:33 +0100 |
wenzelm |
added match_bvars, rename_abs (from thm.ML);
|
file |
diff |
annotate
|
| Wed, 20 Feb 2002 00:53:53 +0100 |
wenzelm |
Symbol.bump_string;
|
file |
diff |
annotate
|
| Thu, 17 Jan 2002 21:03:55 +0100 |
wenzelm |
added add_term_free_names (more precise/efficient than add_term_names);
|
file |
diff |
annotate
|
| Fri, 14 Dec 2001 11:53:31 +0100 |
wenzelm |
added invent_type_names;
|
file |
diff |
annotate
|
| Wed, 28 Nov 2001 00:39:33 +0100 |
wenzelm |
variant: preserve suffix of underscores (for skolem/internal names etc.);
|
file |
diff |
annotate
|
| Wed, 24 Oct 2001 17:38:19 +0200 |
wenzelm |
added lambda;
|
file |
diff |
annotate
|
| Tue, 23 Oct 2001 19:14:13 +0200 |
wenzelm |
replace_dummy_patterns: lift over bounds;
|
file |
diff |
annotate
|
| Thu, 31 May 2001 17:57:02 +0200 |
wenzelm |
invent_names
|
file |
diff |
annotate
|
| Sat, 06 Jan 2001 21:27:33 +0100 |
wenzelm |
added list_abs;
|
file |
diff |
annotate
|
| Wed, 13 Dec 2000 17:41:10 +0100 |
wenzelm |
fixed add_term_names: NameSpace.base;
|
file |
diff |
annotate
|
| Thu, 30 Nov 2000 20:05:54 +0100 |
wenzelm |
added is_replaced_dummy_pattern;
|
file |
diff |
annotate
|
| Tue, 29 Aug 2000 15:13:10 +0200 |
nipkow |
*** empty log message ***
|
file |
diff |
annotate
|
| Fri, 04 Aug 2000 22:59:33 +0200 |
wenzelm |
added dummy_patternN, no_dummy_patterns, replace_dummy_patterns;
|
file |
diff |
annotate
|
| Thu, 13 Jul 2000 23:15:20 +0200 |
wenzelm |
add_term_consts: ins_string;
|
file |
diff |
annotate
|
| Thu, 30 Mar 2000 14:20:01 +0200 |
wenzelm |
foldl_term_types: depend on term as well;
|
file |
diff |
annotate
|
| Fri, 10 Mar 2000 15:00:01 +0100 |
berghofe |
Added functions subst_TVars_Vartab and typ_subst_TVars_Vartab.
|
file |
diff |
annotate
|
| Wed, 29 Sep 1999 13:51:41 +0200 |
wenzelm |
added rems_sort;
|
file |
diff |
annotate
|
| Wed, 01 Sep 1999 21:05:19 +0200 |
wenzelm |
structure Termtab;
|
file |
diff |
annotate
|
| Mon, 23 Aug 1999 09:36:05 +0200 |
nipkow |
Corrected two busg in the simplifier.
|
file |
diff |
annotate
|
| Sat, 10 Jul 1999 21:41:05 +0200 |
wenzelm |
Symtab.lookup_multi;
|
file |
diff |
annotate
|
| Fri, 30 Apr 1999 18:02:16 +0200 |
wenzelm |
val foldl_map_aterms: ('a * term -> 'a * term) -> 'a * term -> 'a * term;
|
file |
diff |
annotate
|
| Fri, 18 Dec 1998 11:01:25 +0100 |
paulson |
moved dest_Type to term.ML from HOL/Tools/primrec_package
|
file |
diff |
annotate
|
| Sun, 29 Nov 1998 13:14:45 +0100 |
wenzelm |
added oct_char;
|
file |
diff |
annotate
|
| Tue, 29 Sep 1998 15:59:43 +0200 |
paulson |
new function inter_term
|
file |
diff |
annotate
|
| Mon, 09 Mar 1998 16:09:32 +0100 |
wenzelm |
tuned some names;
|
file |
diff |
annotate
|
| Wed, 18 Feb 1998 11:31:25 +0100 |
nipkow |
Improved loop-test for rewrite rules a little.
|
file |
diff |
annotate
|
| Thu, 12 Feb 1998 16:54:01 +0100 |
wenzelm |
tuned comments;
|
file |
diff |
annotate
|
| Fri, 06 Feb 1998 11:18:29 +0100 |
wenzelm |
added Vartab: TABLE;
|
file |
diff |
annotate
|
| Sun, 28 Dec 1997 15:24:11 +0100 |
wenzelm |
made MLWorks happy;
|
file |
diff |
annotate
|