| 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
|