| Sat, 05 Nov 2011 22:01:19 +0100 |
misc tuning;
|
file | diff | annotate |
| Sun, 30 Oct 2011 22:20:45 +0100 |
removed obsolete argument (cf. aa35859c8741);
|
file | diff | annotate |
| Sat, 29 Oct 2011 12:57:43 +0200 |
uniform treatment of syntax declaration wrt. aux. context (NB: notation avoids duplicate mixfix internally);
|
file | diff | annotate |
| Fri, 28 Oct 2011 23:16:50 +0200 |
refined Local_Theory.declaration {syntax = false, pervasive} semantics: update is applied to auxiliary context as well;
|
file | diff | annotate |
| Wed, 13 Jul 2011 21:44:15 +0200 |
recovered some runtime sharing from d6b6c74a8bcf, without the global memory bottleneck;
|
file | diff | annotate |
| Wed, 27 Apr 2011 17:58:45 +0200 |
reorganized fixes as specialized (global) name space;
|
file | diff | annotate |
| Sun, 17 Apr 2011 21:42:47 +0200 |
added Binding.print convenience, which includes quote already;
|
file | diff | annotate |
| Sun, 17 Apr 2011 19:54:04 +0200 |
report Name_Space.declare/define, relatively to context;
|
file | diff | annotate |
| Sat, 16 Apr 2011 15:47:52 +0200 |
modernized structure Proof_Context;
|
file | diff | annotate |
| Fri, 08 Apr 2011 14:20:57 +0200 |
discontinued special treatment of structure Mixfix;
|
file | diff | annotate |
| Sun, 13 Mar 2011 22:55:50 +0100 |
tuned headers;
|
file | diff | annotate |
| Fri, 17 Dec 2010 17:08:56 +0100 |
renamed structure MetaSimplifier to raw_Simplifer, to emphasize its meaning;
|
file | diff | annotate |
| Sun, 28 Nov 2010 15:28:48 +0100 |
superficial tuning;
|
file | diff | annotate |
| Mon, 20 Sep 2010 16:05:25 +0200 |
renamed structure PureThy to Pure_Thy and moved most content to Global_Theory, to emphasize that this is global-only;
|
file | diff | annotate |
| Fri, 27 Aug 2010 19:43:28 +0200 |
more careful treatment of context visibility flag wrt. spurious warnings;
|
file | diff | annotate |
| Thu, 26 Aug 2010 15:48:08 +0200 |
renamed Local_Theory.theory(_result) to Local_Theory.background_theory(_result) to emphasize that this belongs to the infrastructure and is rarely appropriate in user-space tools;
|
file | diff | annotate |
| Wed, 11 Aug 2010 12:24:24 +0200 |
moved theory-level target operation fragements to Generic_Target; adjusted bootstrap order
|
file | diff | annotate |
| Tue, 10 Aug 2010 15:09:39 +0200 |
basic renumbering
|
file | diff | annotate |
| Tue, 10 Aug 2010 14:57:58 +0200 |
separated type from term parameters
|
file | diff | annotate |
| Tue, 10 Aug 2010 14:53:41 +0200 |
moved extra_tfrees check for mixfix syntax to Generic_Target
|
file | diff | annotate |
| Tue, 10 Aug 2010 14:47:22 +0200 |
name and argument grouping tuning
|
file | diff | annotate |
| Tue, 10 Aug 2010 14:42:30 +0200 |
whitespace tuning
|
file | diff | annotate |
| Tue, 10 Aug 2010 14:15:44 +0200 |
added generic_target.ML
|
file | diff | annotate |