| 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
|
| 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
|