| Thu, 27 May 2010 17:41:27 +0200 |
wenzelm |
renamed structure TypeInfer to Type_Infer, keeping the old name as legacy alias for some time;
|
file |
diff |
annotate
|
| Tue, 04 May 2010 12:30:15 +0200 |
wenzelm |
simplified/unified fundamental operations on types/terms/proofterms -- prefer Same.operation over "option" variant;
|
file |
diff |
annotate
|
| Mon, 03 May 2010 14:25:56 +0200 |
wenzelm |
renamed ProofContext.init to ProofContext.init_global to emphasize that this is not the real thing;
|
file |
diff |
annotate
|
| Fri, 30 Apr 2010 23:53:37 +0200 |
wenzelm |
renamed Variable.thm_context to Variable.global_thm_context to emphasize that this is not the real thing;
|
file |
diff |
annotate
|
| Wed, 25 Nov 2009 09:13:46 +0100 |
haftmann |
normalized uncurry take/drop
|
file |
diff |
annotate
|
| Tue, 24 Nov 2009 17:28:25 +0100 |
haftmann |
curried take/drop
|
file |
diff |
annotate
|
| Sun, 08 Nov 2009 16:30:41 +0100 |
wenzelm |
adapted Generic_Data, Proof_Data;
|
file |
diff |
annotate
|
| Wed, 21 Oct 2009 12:09:37 +0200 |
haftmann |
curried inter as canonical list operation (beware of argument order)
|
file |
diff |
annotate
|
| Wed, 21 Oct 2009 08:14:38 +0200 |
haftmann |
dropped redundant gen_ prefix
|
file |
diff |
annotate
|
| Tue, 20 Oct 2009 16:13:01 +0200 |
haftmann |
replaced old_style infixes eq_set, subset, union, inter and variants by generic versions
|
file |
diff |
annotate
|
| Wed, 30 Sep 2009 22:20:58 +0200 |
wenzelm |
eliminated redundant bindings;
|
file |
diff |
annotate
|
| Thu, 30 Jul 2009 01:14:40 +0200 |
wenzelm |
Variable.importT/import: return full instantiations, tuned;
|
file |
diff |
annotate
|
| Sun, 26 Jul 2009 13:12:54 +0200 |
wenzelm |
Variable.focus: named parameters;
|
file |
diff |
annotate
|
| Thu, 09 Jul 2009 22:48:12 +0200 |
wenzelm |
renamed structure TermSubst to Term_Subst;
|
file |
diff |
annotate
|
| Wed, 24 Jun 2009 21:28:02 +0200 |
wenzelm |
renamed Variable.import_thms to Variable.import (back again cf. ed7aa5a350ef -- Alice is no longer supported);
|
file |
diff |
annotate
|
| Sat, 28 Mar 2009 16:30:09 +0100 |
wenzelm |
replaced add_binds by singleton bind_term;
|
file |
diff |
annotate
|
| Wed, 21 Jan 2009 22:26:49 +0100 |
wenzelm |
eliminated obsolete var morphism;
|
file |
diff |
annotate
|
| Wed, 31 Dec 2008 19:54:04 +0100 |
wenzelm |
Term.declare_typ_names, Term.declare_term_frees;
|
file |
diff |
annotate
|
| Thu, 04 Dec 2008 14:43:33 +0100 |
haftmann |
cleaned up binding module and related code
|
file |
diff |
annotate
|
| Thu, 16 Oct 2008 22:44:34 +0200 |
wenzelm |
maintain sort occurrences of declared terms;
|
file |
diff |
annotate
|
| Thu, 19 Jun 2008 20:48:04 +0200 |
wenzelm |
added declare_typ;
|
file |
diff |
annotate
|
| Tue, 10 Jun 2008 16:43:21 +0200 |
wenzelm |
focus: actually declare constraints for local parameters;
|
file |
diff |
annotate
|
| Thu, 17 Apr 2008 22:22:26 +0200 |
wenzelm |
variant_fixes: preserve internal state, mark skolem only for body mode;
|
file |
diff |
annotate
|
| Fri, 07 Dec 2007 15:08:08 +0100 |
haftmann |
exported declare_names
|
file |
diff |
annotate
|
| Wed, 07 Nov 2007 16:42:57 +0100 |
wenzelm |
refined notion of consts within the local scope;
|
file |
diff |
annotate
|
| Tue, 06 Nov 2007 22:50:34 +0100 |
wenzelm |
added is_const/declare_const for local scope of fixes/consts;
|
file |
diff |
annotate
|
| Tue, 16 Oct 2007 17:06:15 +0200 |
wenzelm |
add_bind: close_schematic_term;
|
file |
diff |
annotate
|
| Thu, 04 Oct 2007 20:29:24 +0200 |
wenzelm |
replaced literal 'a by Name.aT;
|
file |
diff |
annotate
|
| Sat, 29 Sep 2007 21:39:50 +0200 |
wenzelm |
maintain maxidx (analogous to name context);
|
file |
diff |
annotate
|
| Wed, 26 Sep 2007 11:27:46 +0200 |
wenzelm |
declare_constraints: declare (fix) type variables within constraints, but not terms themselves;
|
file |
diff |
annotate
|
| Mon, 24 Sep 2007 21:07:39 +0200 |
wenzelm |
added polymorphic_types;
|
file |
diff |
annotate
|
| Mon, 07 May 2007 00:49:59 +0200 |
wenzelm |
simplified DataFun interfaces;
|
file |
diff |
annotate
|
| Sun, 15 Apr 2007 23:25:54 +0200 |
wenzelm |
removed obsolete redeclare_skolems;
|
file |
diff |
annotate
|
| Sun, 15 Apr 2007 14:31:47 +0200 |
wenzelm |
Thm.fold_terms;
|
file |
diff |
annotate
|
| Sat, 14 Apr 2007 00:46:21 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Wed, 04 Apr 2007 23:29:41 +0200 |
wenzelm |
renamed Variable.importT to importT_thms;
|
file |
diff |
annotate
|
| Tue, 03 Apr 2007 19:24:13 +0200 |
wenzelm |
renamed Variable.import to import_thms (avoid clash with Alice keywords);
|
file |
diff |
annotate
|
| 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
|