| Mon, 06 Apr 2015 17:06:48 +0200 |
wenzelm |
@{command_spec} is superseded by @{command_keyword};
|
file |
diff |
annotate
|
| Sun, 29 Mar 2015 19:23:08 +0200 |
wenzelm |
proper local Proof_Context.arity_sorts;
|
file |
diff |
annotate
|
| Wed, 26 Nov 2014 20:05:34 +0100 |
wenzelm |
renamed "pairself" to "apply2", in accordance to @{apply 2};
|
file |
diff |
annotate
|
| Mon, 03 Nov 2014 14:50:27 +0100 |
wenzelm |
eliminated unused int_only flag (see also c12484a27367);
|
file |
diff |
annotate
|
| Wed, 29 Oct 2014 19:01:49 +0100 |
wenzelm |
modernized setup;
|
file |
diff |
annotate
|
| Mon, 31 Mar 2014 12:35:39 +0200 |
wenzelm |
some shortcuts for chunks, which sometimes avoid bulky string output;
|
file |
diff |
annotate
|
| Thu, 06 Mar 2014 13:44:01 +0100 |
wenzelm |
more uniform check_const/read_const;
|
file |
diff |
annotate
|
| Wed, 26 Feb 2014 10:53:19 +0100 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Mon, 03 Feb 2014 19:50:16 +0100 |
wenzelm |
unused;
|
file |
diff |
annotate
|
| Mon, 03 Feb 2014 16:33:54 +0100 |
wenzelm |
more formal markup;
|
file |
diff |
annotate
|
| Mon, 03 Feb 2014 15:44:46 +0100 |
wenzelm |
clarified error messages: Pretty.str is for atomic/unformatted strings only, accumulate buffer of formatted strings instead;
|
file |
diff |
annotate
|
| Mon, 03 Feb 2014 15:31:47 +0100 |
wenzelm |
just error, not a failed attempt to raise an exception;
|
file |
diff |
annotate
|
| Mon, 03 Feb 2014 15:28:01 +0100 |
wenzelm |
tuned whitespace;
|
file |
diff |
annotate
|
| Tue, 26 Nov 2013 10:17:14 +0100 |
traytel |
made SML/NJ happier
|
file |
diff |
annotate
|
| Mon, 25 Nov 2013 15:56:23 +0100 |
traytel |
possibility to fold coercion inference error messages; tuned;
|
file |
diff |
annotate
|
| Mon, 18 Nov 2013 14:57:28 +0100 |
traytel |
show all involved subtyping constraints that cause coercion inference to fail
|
file |
diff |
annotate
|
| Wed, 11 Sep 2013 15:42:05 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Sun, 23 Jun 2013 22:31:50 +0200 |
wenzelm |
tuned message -- more markup;
|
file |
diff |
annotate
|
| Tue, 05 Mar 2013 09:47:15 +0100 |
traytel |
allow more general coercion maps; tuned;
|
file |
diff |
annotate
|
| Mon, 04 Mar 2013 09:57:54 +0100 |
traytel |
tuned (extend datatype to inline option)
|
file |
diff |
annotate
|
| Fri, 01 Mar 2013 22:15:31 +0100 |
traytel |
constants with coercion-invariant arguments (possibility to disable/reenable
|
file |
diff |
annotate
|
| Fri, 22 Feb 2013 13:39:47 +0100 |
traytel |
tuned error messages
|
file |
diff |
annotate
|
| Fri, 22 Feb 2013 13:36:31 +0100 |
traytel |
apply unifying substitution before building the constraint graph
|
file |
diff |
annotate
|
| Sat, 29 Sep 2012 18:23:46 +0200 |
wenzelm |
more explicit Syntax_Trans.mark_bound_abs/mark_bound_body: preserve type information for show_markup;
|
file |
diff |
annotate
|
| Tue, 25 Sep 2012 18:24:49 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Tue, 25 Sep 2012 14:32:41 +0200 |
wenzelm |
added graph encode/decode operations;
|
file |
diff |
annotate
|
| Wed, 05 Sep 2012 10:53:51 +0200 |
traytel |
more conservative rechecking of processed constraints in subtyping constraint simplification
|
file |
diff |
annotate
|
| Wed, 21 Mar 2012 11:00:34 +0100 |
wenzelm |
prefer explicitly qualified exception List.Empty;
|
file |
diff |
annotate
|
| Fri, 16 Mar 2012 18:20:12 +0100 |
wenzelm |
outer syntax command definitions based on formal command_spec derived from theory header declarations;
|
file |
diff |
annotate
|
| Sat, 25 Feb 2012 12:34:56 +0100 |
wenzelm |
discontinued slightly odd Graph.del_nodes (inefficient due to full Table.map);
|
file |
diff |
annotate
|