| Thu, 11 Oct 2012 16:09:44 +0200 |
wenzelm |
refrain from quantifying outer fixes, to enable nesting of contexts like "context fixes x context assumes A x";
|
file |
diff |
annotate
|
| Thu, 11 Oct 2012 15:26:33 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Thu, 11 Oct 2012 15:06:27 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Tue, 09 Oct 2012 20:23:58 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Tue, 03 Apr 2012 20:24:00 +0200 |
wenzelm |
avoid duplicate PIDE markup;
|
file |
diff |
annotate
|
| Tue, 03 Apr 2012 18:22:14 +0200 |
wenzelm |
close context elements via Expression.cert/read_declaration;
|
file |
diff |
annotate
|
| Tue, 03 Apr 2012 11:21:17 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Sun, 01 Apr 2012 19:07:32 +0200 |
wenzelm |
added Attrib.global_notes/local_notes/generic_notes convenience;
|
file |
diff |
annotate
|
| Wed, 21 Mar 2012 21:24:13 +0100 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Wed, 14 Mar 2012 17:52:38 +0100 |
wenzelm |
source positions for locale and class expressions;
|
file |
diff |
annotate
|
| Tue, 13 Mar 2012 14:17:42 +0100 |
wenzelm |
refined 'interpret': reset facts ("this") and print_result, which merely consist of internal / protected statement;
|
file |
diff |
annotate
|
| Sat, 10 Mar 2012 20:02:15 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Sat, 10 Mar 2012 17:07:10 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Sat, 19 Nov 2011 16:16:33 +0100 |
wenzelm |
simplified Locale.add_thmss, after partial evaluation of attributes;
|
file |
diff |
annotate
|
| Sat, 19 Nov 2011 15:34:37 +0100 |
wenzelm |
misc tuning;
|
file |
diff |
annotate
|
| Sat, 19 Nov 2011 15:04:36 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Fri, 28 Oct 2011 17:15:52 +0200 |
wenzelm |
tuned signature -- refined terminology;
|
file |
diff |
annotate
|
| Fri, 28 Oct 2011 15:38:41 +0200 |
wenzelm |
slightly more explicit/syntactic modelling of morphisms;
|
file |
diff |
annotate
|
| Sat, 25 Jun 2011 12:19:54 +0200 |
ballarin |
While reading equations of an interpretation, already allow syntax provided by the interpretation base.
|
file |
diff |
annotate
|
| Wed, 27 Apr 2011 20:58:40 +0200 |
wenzelm |
tuned signature -- eliminated odd comment;
|
file |
diff |
annotate
|
| Wed, 27 Apr 2011 10:31:18 +0200 |
wenzelm |
more uniform Variable.add_frees/add_fixed etc.;
|
file |
diff |
annotate
|
| Thu, 21 Apr 2011 12:56:27 +0200 |
wenzelm |
discontinuend obsolete Thm.definitionK, which was hardly ever well-defined;
|
file |
diff |
annotate
|
| Sun, 17 Apr 2011 21:42:47 +0200 |
wenzelm |
added Binding.print convenience, which includes quote already;
|
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 15:25:25 +0200 |
wenzelm |
prefer local name spaces;
|
file |
diff |
annotate
|
| Sat, 16 Apr 2011 13:48:45 +0200 |
wenzelm |
Name_Space: proper configuration options long_names, short_names, unique_names instead of former unsynchronized references;
|
file |
diff |
annotate
|
| Sat, 16 Apr 2011 12:46:18 +0200 |
wenzelm |
tuned signature, disentangled dependencies;
|
file |
diff |
annotate
|
| Fri, 08 Apr 2011 16:34:14 +0200 |
wenzelm |
discontinued special treatment of structure Lexicon;
|
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
|