| Sun, 01 Apr 2012 19:07:32 +0200 |
wenzelm |
added Attrib.global_notes/local_notes/generic_notes convenience;
|
file |
diff |
annotate
|
| Sun, 18 Mar 2012 13:04:22 +0100 |
wenzelm |
maintain generic context naming in structure Name_Space (NB: empty = default_naming, init = local_naming);
|
file |
diff |
annotate
|
| Tue, 13 Mar 2012 17:04:00 +0100 |
wenzelm |
suppress vacous notes elements, with subtle change of semantics: 'interpret' no longer pulls-in unnamed facts "by fact";
|
file |
diff |
annotate
|
| Tue, 13 Mar 2012 16:22:18 +0100 |
wenzelm |
improved attribute "abs_def" to handle object-equality as well;
|
file |
diff |
annotate
|
| Sat, 03 Mar 2012 21:43:59 +0100 |
wenzelm |
canonical argument order for attribute application;
|
file |
diff |
annotate
|
| Fri, 17 Feb 2012 15:42:26 +0100 |
wenzelm |
simplified configuration options for syntax ambiguity;
|
file |
diff |
annotate
|
| Thu, 16 Feb 2012 22:18:28 +0100 |
wenzelm |
simplified configuration options for syntax ambiguity;
|
file |
diff |
annotate
|
| Thu, 05 Jan 2012 20:26:01 +0100 |
wenzelm |
discontinued Syntax.positions -- atomic parse trees are always annotated;
|
file |
diff |
annotate
|
| Wed, 23 Nov 2011 22:07:55 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Mon, 21 Nov 2011 23:03:31 +0100 |
wenzelm |
drop vacuous decls;
|
file |
diff |
annotate
|
| Sat, 19 Nov 2011 14:31:43 +0100 |
wenzelm |
refined partial evaluation of attributes: avoid duplication of facts for plain declarations;
|
file |
diff |
annotate
|
| Sat, 19 Nov 2011 13:02:50 +0100 |
wenzelm |
do not store vacuous theorem specifications -- relevant for frugal local theory content;
|
file |
diff |
annotate
|
| Thu, 17 Nov 2011 21:31:29 +0100 |
wenzelm |
partial evaluation in invisible context;
|
file |
diff |
annotate
|
| Wed, 16 Nov 2011 23:09:46 +0100 |
wenzelm |
retain mixed attributes as dynamic theorem expression, but disallow subsequent static rules;
|
file |
diff |
annotate
|
| Wed, 16 Nov 2011 21:16:36 +0100 |
wenzelm |
clarified Attrib.partial_evaluation;
|
file |
diff |
annotate
|
| Mon, 14 Nov 2011 23:00:56 +0100 |
wenzelm |
some support for partial evaluation of attributed facts;
|
file |
diff |
annotate
|
| Mon, 14 Nov 2011 19:27:42 +0100 |
wenzelm |
eliminated dead code;
|
file |
diff |
annotate
|
| Mon, 07 Nov 2011 17:00:23 +0100 |
wenzelm |
tuned signature -- avoid spurious Thm.mixed_attribute;
|
file |
diff |
annotate
|
| Sun, 06 Nov 2011 21:51:46 +0100 |
wenzelm |
more explicit representation of rule_attribute vs. declaration_attribute vs. mixed_attribute;
|
file |
diff |
annotate
|
| Sat, 06 Aug 2011 15:48:08 +0200 |
kleing |
make syntax ambiguity warnings a config option
|
file |
diff |
annotate
|
| Mon, 08 Aug 2011 13:39:51 +0200 |
wenzelm |
made SML/NJ happy;
|
file |
diff |
annotate
|
| Sat, 06 Aug 2011 14:16:23 +0200 |
nipkow |
extended user-level attribute case_names with names for case hypotheses
|
file |
diff |
annotate
|
| Fri, 10 Jun 2011 11:47:52 +0200 |
wenzelm |
tuned name (cf. blast_stats);
|
file |
diff |
annotate
|
| Sun, 15 May 2011 17:06:35 +0200 |
wenzelm |
optional description for 'attribute_setup' and 'method_setup';
|
file |
diff |
annotate
|
| Sat, 14 May 2011 18:29:06 +0200 |
wenzelm |
discontinued global config options within attribute name space;
|
file |
diff |
annotate
|
| Tue, 03 May 2011 22:27:32 +0200 |
wenzelm |
more conventional naming scheme: names_long, names_short, names_unique;
|
file |
diff |
annotate
|
| Mon, 02 May 2011 16:33:21 +0200 |
wenzelm |
added Attrib.setup_config_XXX conveniences, with implicit setup of the background theory;
|
file |
diff |
annotate
|
| Sun, 17 Apr 2011 21:17:45 +0200 |
wenzelm |
markup attributes/methods via name space;
|
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
|