| Tue, 12 Dec 2006 20:49:26 +0100 |
wenzelm |
tuned expand_binds;
|
file |
diff |
annotate
|
| Wed, 06 Dec 2006 21:19:00 +0100 |
wenzelm |
moved hidden_polymorphism to term.ML;
|
file |
diff |
annotate
|
| Tue, 28 Nov 2006 00:35:28 +0100 |
wenzelm |
added add_fixed;
|
file |
diff |
annotate
|
| Fri, 24 Nov 2006 22:05:18 +0100 |
wenzelm |
added export_morphism;
|
file |
diff |
annotate
|
| Tue, 14 Nov 2006 22:17:00 +0100 |
wenzelm |
removed fix_frees interface;
|
file |
diff |
annotate
|
| Tue, 14 Nov 2006 00:16:30 +0100 |
wenzelm |
declare_constraints: reset constraint on dummyS;
|
file |
diff |
annotate
|
| Fri, 10 Nov 2006 10:42:25 +0100 |
wenzelm |
tuned Variable.trade;
|
file |
diff |
annotate
|
| Sat, 30 Sep 2006 21:39:17 +0200 |
wenzelm |
renamed Variable.invent_fixes to Variable.variant_fixes;
|
file |
diff |
annotate
|
| Mon, 18 Sep 2006 19:39:07 +0200 |
wenzelm |
Thm.dest_arg;
|
file |
diff |
annotate
|
| Tue, 12 Sep 2006 12:12:46 +0200 |
wenzelm |
moved term subst functions to TermSubst;
|
file |
diff |
annotate
|
| Wed, 02 Aug 2006 22:26:57 +0200 |
wenzelm |
normalized Proof.context/method type aliases;
|
file |
diff |
annotate
|
| Sun, 30 Jul 2006 21:28:55 +0200 |
wenzelm |
export: refrain from adjusting maxidx;
|
file |
diff |
annotate
|
| Sat, 29 Jul 2006 00:51:33 +0200 |
wenzelm |
added add_fixes_direct;
|
file |
diff |
annotate
|
| Thu, 27 Jul 2006 23:28:25 +0200 |
wenzelm |
added fix_frees (from Isar/proof_context.ML);
|
file |
diff |
annotate
|
| Wed, 26 Jul 2006 19:37:43 +0200 |
wenzelm |
import(T): result includes fixed types/terms;
|
file |
diff |
annotate
|
| Tue, 25 Jul 2006 21:18:05 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Wed, 19 Jul 2006 12:12:05 +0200 |
wenzelm |
reorganize declarations (more efficient);
|
file |
diff |
annotate
|
| Tue, 18 Jul 2006 20:01:45 +0200 |
wenzelm |
added newly_fixed, focus;
|
file |
diff |
annotate
|
| Thu, 13 Jul 2006 13:42:02 +0200 |
wenzelm |
Name.context already declares empty names;
|
file |
diff |
annotate
|
| Tue, 11 Jul 2006 23:00:39 +0200 |
wenzelm |
separate names filed (covers fixes/defaults);
|
file |
diff |
annotate
|
| Tue, 11 Jul 2006 12:17:09 +0200 |
wenzelm |
maintain Name.context for fixes/defaults;
|
file |
diff |
annotate
|
| Tue, 04 Jul 2006 19:49:54 +0200 |
wenzelm |
polymorphic: always generalize wrt. used_types;
|
file |
diff |
annotate
|
| Mon, 19 Jun 2006 20:21:32 +0200 |
wenzelm |
added declare_thm, thm_context;
|
file |
diff |
annotate
|
| Sat, 17 Jun 2006 19:37:52 +0200 |
wenzelm |
major reworking of export functionality -- based on Term/Thm.generalize;
|
file |
diff |
annotate
|
| Thu, 15 Jun 2006 23:08:58 +0200 |
wenzelm |
Fixed type/term variables and polymorphic term abbreviations.
|
file |
diff |
annotate
|