| Fri, 27 Apr 2012 21:47:47 +0200 |
avoid spurious warning in invisible context, notably Haftmann-Wenzel sandwich;
|
file | diff | annotate |
| Sat, 30 Oct 2010 16:33:58 +0200 |
support for real valued configuration options;
|
file | diff | annotate |
| Mon, 06 Sep 2010 21:33:19 +0200 |
more explicit indication of Config.raw options, which are only needed for bootstrapping Pure;
|
file | diff | annotate |
| Fri, 03 Sep 2010 16:09:12 +0200 |
more explicit Config.declare vs. Config.declare_global;
|
file | diff | annotate |
| Fri, 27 Aug 2010 17:02:19 +0200 |
tuned printed type names, according to ML;
|
file | diff | annotate |
| Mon, 10 May 2010 20:53:06 +0200 |
renamed Config.get_thy to Config.get_global etc. to indicate that this is not the real thing;
|
file | diff | annotate |
| Sun, 28 Mar 2010 17:43:09 +0200 |
pass raw Context.generic, to avoid wasteful Context.proof_of -- Config.get_thy is often used in performance critical spots like unify.ML;
|
file | diff | annotate |
| Sun, 28 Mar 2010 16:13:29 +0200 |
configuration options admit dynamic default values;
|
file | diff | annotate |
| Sun, 08 Nov 2009 16:30:41 +0100 |
adapted Generic_Data, Proof_Data;
|
file | diff | annotate |
| Wed, 21 Jan 2009 23:21:44 +0100 |
removed Ids;
|
file | diff | annotate |
| Thu, 02 Aug 2007 12:06:28 +0200 |
added name_of;
|
file | diff | annotate |
| Wed, 01 Aug 2007 16:55:42 +0200 |
renamed config_option.ML to config.ML;
|
file | diff | annotate |
| Fri, 27 Jul 2007 20:11:47 +0200 |
map_value: dynamic type checking;
|
file | diff | annotate |
| Fri, 27 Jul 2007 16:31:14 +0200 |
exported datatype value;
|
file | diff | annotate |
| Wed, 25 Jul 2007 22:20:49 +0200 |
Configuration options as values within the local context.
|
file | diff | annotate |