| Mon, 24 Sep 2018 19:34:14 +0200 |
wenzelm |
tuned signature: prefer value-oriented pretty-printing;
|
file |
diff |
annotate
|
| Fri, 31 Aug 2018 13:34:31 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Fri, 02 Mar 2018 15:14:59 +0100 |
ballarin |
Drop illegitimate optimisation from d5a7f2c54655.
|
file |
diff |
annotate
|
| Fri, 02 Mar 2018 14:28:39 +0100 |
ballarin |
Fall back to reading rewrite morphism first if activation fails without it.
|
file |
diff |
annotate
|
| Fri, 02 Mar 2018 14:19:25 +0100 |
ballarin |
Proper rewrite morphisms in locale instances.
|
file |
diff |
annotate
|
| Fri, 23 Feb 2018 21:12:08 +0100 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Fri, 23 Feb 2018 20:55:46 +0100 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Wed, 21 Feb 2018 20:13:42 +0100 |
wenzelm |
more standard instantiate operations, where substitutions are already certified and stored with trimmed theory certificate;
|
file |
diff |
annotate
|
| Wed, 21 Feb 2018 16:26:42 +0100 |
wenzelm |
minor tuning and clarification;
|
file |
diff |
annotate
|
| Tue, 20 Feb 2018 23:23:40 +0100 |
wenzelm |
minor tuning and clarification;
|
file |
diff |
annotate
|
| Tue, 20 Feb 2018 23:03:28 +0100 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Mon, 19 Feb 2018 22:07:21 +0100 |
wenzelm |
support for lazy notes in global/local context and Element.Lazy_Notes: name binding and fact without attributes;
|
file |
diff |
annotate
|
| Mon, 19 Feb 2018 15:41:17 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Tue, 16 Jan 2018 19:28:05 +0100 |
ballarin |
Experimental support for rewrite morphisms in locale instances.
|
file |
diff |
annotate
|
| Fri, 04 Aug 2017 08:12:37 +0200 |
haftmann |
provide explicit variant initializers for regular named target vs. almost-named target
|
file |
diff |
annotate
|
| Wed, 06 Jul 2016 11:29:51 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Tue, 05 Jul 2016 14:20:27 +0200 |
wenzelm |
PIDE reports of implicit variable scope;
|
file |
diff |
annotate
|
| Thu, 23 Jun 2016 11:01:14 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Thu, 12 May 2016 10:57:09 +0200 |
wenzelm |
avoid spurious fact index, notably in "context begin" (via Bundle.context);
|
file |
diff |
annotate
|
| Thu, 12 May 2016 10:21:59 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Thu, 12 May 2016 10:16:52 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Tue, 12 Apr 2016 14:38:57 +0200 |
wenzelm |
Type_Infer.object_logic controls improvement of type inference result;
|
file |
diff |
annotate
|
| Tue, 29 Mar 2016 21:17:29 +0200 |
wenzelm |
more position information for type mixfix;
|
file |
diff |
annotate
|
| Sat, 14 Nov 2015 08:45:51 +0100 |
haftmann |
separate ML module for interpretation
|
file |
diff |
annotate
|
| Tue, 06 Oct 2015 13:31:44 +0200 |
wenzelm |
just one theorem kind, which is legacy anyway;
|
file |
diff |
annotate
|
| Wed, 02 Sep 2015 16:01:57 +0200 |
wenzelm |
expose locale definition to normal user-namespace (for completion, query etc.) -- in contrast to 149f80f27c84, ba9f52f56356, f7d9c5e5d2f9;
|
file |
diff |
annotate
|
| Sun, 16 Aug 2015 19:25:08 +0200 |
wenzelm |
added Thm.chyps_of;
|
file |
diff |
annotate
|
| Thu, 13 Aug 2015 11:05:19 +0200 |
wenzelm |
tuned signature, in accordance to sortBy in Scala;
|
file |
diff |
annotate
|
| Sun, 14 Jun 2015 23:22:08 +0200 |
wenzelm |
improved treatment of Element.Obtains via Expression.prepare_stmt;
|
file |
diff |
annotate
|
| Sun, 14 Jun 2015 20:10:21 +0200 |
wenzelm |
clarified context;
|
file |
diff |
annotate
|
| Tue, 09 Jun 2015 16:42:17 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Sun, 07 Jun 2015 20:03:40 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Wed, 08 Apr 2015 19:39:08 +0200 |
wenzelm |
proper context for Object_Logic operations;
|
file |
diff |
annotate
|
| Tue, 31 Mar 2015 00:11:54 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Fri, 06 Mar 2015 17:32:20 +0100 |
wenzelm |
clarified context;
|
file |
diff |
annotate
|
| Fri, 06 Mar 2015 15:58:56 +0100 |
wenzelm |
Thm.cterm_of and Thm.ctyp_of operate on local context;
|
file |
diff |
annotate
|
| Thu, 05 Mar 2015 13:28:04 +0100 |
wenzelm |
tuned -- more explicit use of context;
|
file |
diff |
annotate
|
| Wed, 04 Mar 2015 19:53:18 +0100 |
wenzelm |
tuned signature -- prefer qualified names;
|
file |
diff |
annotate
|
| Sun, 01 Mar 2015 23:35:41 +0100 |
wenzelm |
added Proof_Context.cterm_of/ctyp_of convenience;
|
file |
diff |
annotate
|
| Mon, 05 Jan 2015 18:39:32 +0100 |
haftmann |
formal pretty bodies for class specifications, accepting additional formal bookkeeping in locale.ML
|
file |
diff |
annotate
|
| Sun, 09 Nov 2014 14:08:00 +0100 |
wenzelm |
proper context for compose_tac, Splitter.split_tac (relevant for unify trace options);
|
file |
diff |
annotate
|
| Wed, 13 Aug 2014 13:30:28 +0200 |
wenzelm |
load local_theory.ML before attrib.ML, with subtle change of semantics due to canonical Local_Theory.map_contexts instead of private Local_Theory.map_top;
|
file |
diff |
annotate
|
| Tue, 05 Aug 2014 12:14:25 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Fri, 06 Jun 2014 19:19:46 +0200 |
haftmann |
dropped obscure and unused ad-hoc before_exit hook for named targets
|
file |
diff |
annotate
|
| 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
|