| Thu, 01 May 2014 09:30:34 +0200 |
haftmann |
prevent subscription in nested contexts explicitly -- at foundational and user level
|
file |
diff |
annotate
|
| Fri, 25 Apr 2014 21:45:04 +0200 |
haftmann |
subscription as target-specific implementation device
|
file |
diff |
annotate
|
| Wed, 12 Mar 2014 10:42:28 +0100 |
wenzelm |
more explicit Sign.change_check -- detect structural mistakes where they emerge, not at later theory merges;
|
file |
diff |
annotate
|
| Sat, 08 Mar 2014 21:08:10 +0100 |
wenzelm |
modernized Attrib.check_name/check_src similar to methods (see also a989bdaf8121);
|
file |
diff |
annotate
|
| Thu, 20 Feb 2014 23:16:33 +0100 |
wenzelm |
tuned whitespace;
|
file |
diff |
annotate
|
| Tue, 31 Dec 2013 14:29:16 +0100 |
wenzelm |
proper context for norm_hhf and derived operations;
|
file |
diff |
annotate
|
| Mon, 30 Dec 2013 12:43:06 +0100 |
wenzelm |
tuned whitespace;
|
file |
diff |
annotate
|
| Sun, 29 Dec 2013 23:21:14 +0100 |
haftmann |
simplified
|
file |
diff |
annotate
|
| Sun, 29 Dec 2013 23:21:13 +0100 |
haftmann |
more compact representation of different situations for interpretation
|
file |
diff |
annotate
|
| Sun, 29 Dec 2013 23:21:12 +0100 |
haftmann |
more succint formulation of special case
|
file |
diff |
annotate
|
| Sun, 29 Dec 2013 23:21:11 +0100 |
haftmann |
tuned whitespace
|
file |
diff |
annotate
|
| Wed, 25 Dec 2013 22:35:28 +0100 |
haftmann |
ephemeral interpretation also formally works on theory level
|
file |
diff |
annotate
|
| Sat, 14 Dec 2013 17:28:05 +0100 |
wenzelm |
proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
|
file |
diff |
annotate
|
| Fri, 13 Dec 2013 20:20:15 +0100 |
wenzelm |
maintain morphism names for diagnostic purposes;
|
file |
diff |
annotate
|
| Sat, 23 Nov 2013 17:07:36 +0100 |
wenzelm |
more accurate goal context;
|
file |
diff |
annotate
|
| Fri, 16 Aug 2013 20:58:15 +0200 |
wenzelm |
more markup -- avoid old Locale.extern;
|
file |
diff |
annotate
|
| Sat, 27 Jul 2013 16:35:51 +0200 |
wenzelm |
standardized aliases;
|
file |
diff |
annotate
|
| Thu, 30 May 2013 12:35:40 +0200 |
wenzelm |
standardized aliases;
|
file |
diff |
annotate
|
| Sun, 26 May 2013 19:45:54 +0200 |
haftmann |
more specific structure for registration into theory and dependency onto locale
|
file |
diff |
annotate
|
| Sat, 25 May 2013 18:30:38 +0200 |
wenzelm |
merged
|
file |
diff |
annotate
|
| Sat, 25 May 2013 15:37:53 +0200 |
wenzelm |
syntax translations always depend on context;
|
file |
diff |
annotate
|
| Sat, 25 May 2013 15:44:08 +0200 |
haftmann |
tuned structure
|
file |
diff |
annotate
|
| Wed, 22 May 2013 22:56:17 +0200 |
haftmann |
interpretation must always operate on the last element in a local theory stack, not on all elements: interpretated facts must disappear after pop from local theory stack, and transfer from last target is not enough
|
file |
diff |
annotate
|
| Wed, 22 May 2013 22:56:17 +0200 |
haftmann |
mark local theory as brittle also after interpretation inside locales;
|
file |
diff |
annotate
|
| Wed, 24 Apr 2013 11:32:54 +0200 |
haftmann |
avoid odd reinit after sublocale declaration
|
file |
diff |
annotate
|
| Tue, 23 Apr 2013 19:40:33 +0200 |
haftmann |
dropped dead code
|
file |
diff |
annotate
|
| Tue, 23 Apr 2013 11:14:50 +0200 |
haftmann |
target-sensitive user-level commands interpretation and sublocale
|
file |
diff |
annotate
|
| Tue, 23 Apr 2013 11:14:50 +0200 |
haftmann |
ML interfaces for various kinds of interpretation
|
file |
diff |
annotate
|
| Tue, 23 Apr 2013 11:14:50 +0200 |
haftmann |
tuned
|
file |
diff |
annotate
|
| Sun, 21 Apr 2013 20:08:13 +0200 |
haftmann |
more sharing
|
file |
diff |
annotate
|
| Sun, 21 Apr 2013 16:29:40 +0200 |
haftmann |
interpretation: distinguish theories and proofs by explicit parameter rather than generic context;
|
file |
diff |
annotate
|
| Sun, 21 Apr 2013 10:41:18 +0200 |
haftmann |
dropped unusued identifier
|
file |
diff |
annotate
|
| Sun, 21 Apr 2013 10:41:18 +0200 |
haftmann |
avoid odd bifurcation with Attrib.local_notes vs. Locale.add_thmss -- n.b. note_eqns_dependency operates in a specific locale target
|
file |
diff |
annotate
|
| Sun, 21 Apr 2013 10:41:18 +0200 |
haftmann |
tuned for uniformity
|
file |
diff |
annotate
|
| Wed, 27 Mar 2013 22:36:03 +0100 |
ballarin |
Improvements to the print_dependencies command.
|
file |
diff |
annotate
|
| Thu, 11 Oct 2012 19:25:36 +0200 |
wenzelm |
refined aprop_tr' -- retain entity information by using type slot as adhoc marker;
|
file |
diff |
annotate
|
| 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
|