| Tue, 27 Jan 2009 00:29:37 +0100 |
wenzelm |
proof_body: turned lazy into future -- ensures that body is fulfilled eventually, without explicit force;
|
file |
diff |
annotate
|
| Wed, 31 Dec 2008 18:53:16 +0100 |
wenzelm |
moved old add_type_XXX, add_term_XXX etc. to structure OldTerm;
|
file |
diff |
annotate
|
| Wed, 31 Dec 2008 00:08:13 +0100 |
wenzelm |
moved old add_term_vars, add_term_frees etc. to structure OldTerm;
|
file |
diff |
annotate
|
| Tue, 30 Dec 2008 21:47:11 +0100 |
wenzelm |
canonical Term.add_var_names, Term.add_tvar_namesT;
|
file |
diff |
annotate
|
| Sun, 16 Nov 2008 18:19:27 +0100 |
berghofe |
- Corrected order of quantification over Frees.
|
file |
diff |
annotate
|
| Sat, 15 Nov 2008 21:31:32 +0100 |
wenzelm |
adapted PThm;
|
file |
diff |
annotate
|
| Mon, 23 Jun 2008 23:45:39 +0200 |
wenzelm |
Logic.all/mk_equals/mk_implies;
|
file |
diff |
annotate
|
| Sun, 18 May 2008 15:04:09 +0200 |
wenzelm |
moved global pretty/string_of functions from Sign to Syntax;
|
file |
diff |
annotate
|
| Wed, 19 Mar 2008 07:20:32 +0100 |
haftmann |
Type.lookup now curried
|
file |
diff |
annotate
|
| Tue, 30 Oct 2007 17:58:03 +0100 |
berghofe |
Handle Subscript exception when looking up bound variables.
|
file |
diff |
annotate
|
| Thu, 31 May 2007 23:47:36 +0200 |
wenzelm |
simplified/unified list fold;
|
file |
diff |
annotate
|
| Tue, 05 Dec 2006 00:30:38 +0100 |
wenzelm |
thm/prf: separate official name vs. additional tags;
|
file |
diff |
annotate
|
| Tue, 31 Oct 2006 09:29:06 +0100 |
haftmann |
fixed type signature of Type.varify
|
file |
diff |
annotate
|
| Thu, 21 Sep 2006 19:05:56 +0200 |
wenzelm |
member (op =);
|
file |
diff |
annotate
|
| Fri, 15 Sep 2006 22:56:13 +0200 |
wenzelm |
renamed Term.map_term_types to Term.map_types (cf. Term.fold_types);
|
file |
diff |
annotate
|
| Wed, 02 Aug 2006 22:27:06 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Sun, 11 Jun 2006 21:59:17 +0200 |
wenzelm |
avoid unqualified exception;
|
file |
diff |
annotate
|
| Thu, 27 Apr 2006 15:06:35 +0200 |
wenzelm |
tuned basic list operators (flat, maps, map_filter);
|
file |
diff |
annotate
|
| Wed, 26 Apr 2006 22:38:05 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Thu, 13 Apr 2006 12:00:56 +0200 |
wenzelm |
ignore sorts of consts declarations;
|
file |
diff |
annotate
|
| Tue, 21 Mar 2006 12:18:15 +0100 |
wenzelm |
avoid polymorphic equality;
|
file |
diff |
annotate
|
| Mon, 06 Feb 2006 20:58:54 +0100 |
wenzelm |
Envir.(beta_)eta_contract;
|
file |
diff |
annotate
|
| Wed, 16 Nov 2005 17:45:30 +0100 |
wenzelm |
tuned Pattern.match/unify;
|
file |
diff |
annotate
|
| Thu, 15 Sep 2005 17:16:56 +0200 |
wenzelm |
TableFun/Symtab: curried lookup and update;
|
file |
diff |
annotate
|
| Fri, 02 Sep 2005 15:54:47 +0200 |
haftmann |
some 'assoc' etc. refactoring
|
file |
diff |
annotate
|
| Thu, 01 Sep 2005 22:15:12 +0200 |
wenzelm |
curried_lookup/update;
|
file |
diff |
annotate
|
| Mon, 01 Aug 2005 19:20:37 +0200 |
wenzelm |
replaced atless by term_ord;
|
file |
diff |
annotate
|
| Thu, 28 Jul 2005 15:19:49 +0200 |
wenzelm |
Sign.typ_unify;
|
file |
diff |
annotate
|
| Tue, 19 Jul 2005 17:21:47 +0200 |
wenzelm |
Logic.incr_tvar;
|
file |
diff |
annotate
|
| Fri, 15 Jul 2005 15:44:17 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|