| Wed, 09 Nov 2011 23:16:47 +0100 |
wenzelm |
avoid separate typ_check phases, integrate into main term_check 0 instead (cf. its Syntax.check_typs in Type_Infer_Context.prepare);
|
file |
diff |
annotate
|
| Wed, 09 Nov 2011 22:43:14 +0100 |
wenzelm |
clarified singleton_fixate: intersection with supersort is identity, only replace actual type inference parameters;
|
file |
diff |
annotate
|
| Wed, 09 Nov 2011 21:44:06 +0100 |
wenzelm |
misc tuning and simplification;
|
file |
diff |
annotate
|
| Wed, 09 Nov 2011 20:47:11 +0100 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Wed, 09 Nov 2011 14:15:44 +0100 |
wenzelm |
tuned layout;
|
file |
diff |
annotate
|
| Wed, 27 Apr 2011 20:58:40 +0200 |
wenzelm |
tuned signature -- eliminated odd comment;
|
file |
diff |
annotate
|
| Tue, 19 Apr 2011 14:57:09 +0200 |
wenzelm |
simplified check/uncheck interfaces: result comparison is hardwired by default;
|
file |
diff |
annotate
|
| Sun, 17 Apr 2011 19:54:04 +0200 |
wenzelm |
report Name_Space.declare/define, relatively to context;
|
file |
diff |
annotate
|
| Sat, 16 Apr 2011 15:47:52 +0200 |
wenzelm |
modernized structure Proof_Context;
|
file |
diff |
annotate
|
| Sat, 16 Apr 2011 12:46:18 +0200 |
wenzelm |
tuned signature, disentangled dependencies;
|
file |
diff |
annotate
|
| Sun, 16 Jan 2011 14:57:14 +0100 |
wenzelm |
added before_exit continuation for named targets (locale, class etc.), e.g. for final check/cleanup as in VC management;
|
file |
diff |
annotate
|
| Tue, 26 Oct 2010 14:06:22 +0200 |
haftmann |
consider base sorts of superclasses simultaneously during processing of class specification -- avoids clash of different base sorts
|
file |
diff |
annotate
|
| Mon, 30 Aug 2010 15:19:39 +0200 |
wenzelm |
tuned messages: discontinued spurious full-stops (messages are occasionally composed unexpectedly);
|
file |
diff |
annotate
|
| Thu, 26 Aug 2010 13:09:12 +0200 |
wenzelm |
renamed ProofContext.theory(_result) to ProofContext.background_theory(_result) to emphasize that this belongs to the infrastructure and is rarely appropriate in user-space tools;
|
file |
diff |
annotate
|
| Tue, 17 Aug 2010 17:54:46 +0200 |
haftmann |
enforcing a singleton type inference parameter after type inference and before fixation prevents multiple type variables in import during class declaration
|
file |
diff |
annotate
|
| Fri, 13 Aug 2010 17:17:04 +0200 |
haftmann |
corrected handling of `constrains` elements
|
file |
diff |
annotate
|
| Thu, 12 Aug 2010 13:42:12 +0200 |
haftmann |
named target is optional
|
file |
diff |
annotate
|
| Thu, 12 Aug 2010 13:28:18 +0200 |
haftmann |
Named_Target.init: empty string represents theory target
|
file |
diff |
annotate
|
| Wed, 11 Aug 2010 20:25:44 +0200 |
haftmann |
merged
|
file |
diff |
annotate
| base
|
| Wed, 11 Aug 2010 16:02:03 +0200 |
haftmann |
more convenient split of class modules: class and class_declaration
|
file |
diff |
annotate
| base
|