| Fri, 25 Apr 2025 11:22:25 +0200 |
wenzelm |
more scalable: discontinue odd shortcuts from 6b3739fee456, which produce bulky strings internally;
|
file |
diff |
annotate
|
| Fri, 06 Dec 2024 20:26:33 +0100 |
wenzelm |
clarified renaming of bounds, using Syntax_Trans.variant_bounds: avoid structures and fixed variables with syntax;
|
file |
diff |
annotate
|
| Fri, 06 Dec 2024 13:33:25 +0100 |
wenzelm |
clarified printing of consts: rename apart from all bounds, and thus avoid old Term.declare_free_names with its adhoc policy ("as they are printed");
|
file |
diff |
annotate
|
| Sun, 04 Aug 2024 13:24:54 +0200 |
wenzelm |
tuned: more explicit dest_Type_name and dest_Type_args;
|
file |
diff |
annotate
|
| Wed, 20 Oct 2021 18:13:17 +0200 |
wenzelm |
discontinued obsolete "val extend = I" for data slots;
|
file |
diff |
annotate
|
| Wed, 06 Dec 2017 20:43:09 +0100 |
wenzelm |
prefer control symbol antiquotations;
|
file |
diff |
annotate
|
| 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
|
| Thu, 23 Feb 2012 15:49:40 +0100 |
wenzelm |
clarified Graph.restrict (formerly Graph.subgraph) based on public graph operations;
|
file |
diff |
annotate
|
| Sat, 17 Dec 2011 15:53:58 +0100 |
traytel |
meaningful error message on failing merges of coercion tables
|
file |
diff |
annotate
|
| Wed, 09 Nov 2011 20:47:11 +0100 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Thu, 29 Sep 2011 09:37:59 +0200 |
traytel |
correct coercion generation in case of unknown map functions
|
file |
diff |
annotate
|
| Wed, 17 Aug 2011 19:49:07 +0200 |
traytel |
local coercion insertion algorithm to support complex coercions
|
file |
diff |
annotate
|
| Wed, 17 Aug 2011 19:49:07 +0200 |
traytel |
printing and deleting of coercions
|
file |
diff |
annotate
|
| Sat, 20 Aug 2011 23:35:30 +0200 |
wenzelm |
refined Graph implementation: more abstract/scalable Graph.Keys instead of plain lists -- order of adjacency is now standardized wrt. Key.ord;
|
file |
diff |
annotate
|
| Tue, 28 Jun 2011 10:52:15 +0200 |
traytel |
collapse map functions with identity subcoercions to identities;
|
file |
diff |
annotate
|
| Wed, 08 Jun 2011 15:56:57 +0200 |
wenzelm |
more robust exception pattern General.Subscript;
|
file |
diff |
annotate
|
| Mon, 02 May 2011 16:33:21 +0200 |
wenzelm |
added Attrib.setup_config_XXX conveniences, with implicit setup of the background theory;
|
file |
diff |
annotate
|
| Tue, 19 Apr 2011 20:47:02 +0200 |
wenzelm |
split Type_Infer into early and late part, after Proof_Context;
|
file |
diff |
annotate
|
| Tue, 19 Apr 2011 14:57:09 +0200 |
wenzelm |
simplified check/uncheck interfaces: result comparison is hardwired by default;
|
file |
diff |
annotate
|
| Mon, 18 Apr 2011 20:40:31 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Mon, 18 Apr 2011 13:52:23 +0200 |
wenzelm |
standardized aliases of operations on tsig;
|
file |
diff |
annotate
|
| Mon, 18 Apr 2011 12:11:58 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Mon, 18 Apr 2011 11:13:29 +0200 |
wenzelm |
simplified pretty printing context, which is only required for certain kernel operations;
|
file |
diff |
annotate
|
| Sat, 16 Apr 2011 16:15:37 +0200 |
wenzelm |
modernized structure Proof_Context;
|
file |
diff |
annotate
|
| Fri, 08 Apr 2011 13:31:16 +0200 |
wenzelm |
explicit structure Syntax_Trans;
|
file |
diff |
annotate
|
| Tue, 21 Dec 2010 01:12:14 +0100 |
traytel |
Enabled non fully polymorphic map functions in subtyping
|
file |
diff |
annotate
|
| Fri, 03 Dec 2010 17:59:13 +0100 |
wenzelm |
setup subtyping/coercions once in HOL.thy, but enable it only later via configuration option;
|
file |
diff |
annotate
|
| Thu, 02 Dec 2010 21:48:36 +0100 |
traytel |
use "fold_map" instead of "fold (fn .. => .. (ts @ [t], ..)) .."
|
file |
diff |
annotate
|
| Wed, 01 Dec 2010 13:09:08 +0100 |
wenzelm |
just one Term.dest_funT;
|
file |
diff |
annotate
|
| Wed, 01 Dec 2010 11:06:01 +0100 |
wenzelm |
simplified equality on pairs of types;
|
file |
diff |
annotate
|
| Mon, 29 Nov 2010 16:53:08 +0100 |
traytel |
two-staged architecture for subtyping;
|
file |
diff |
annotate
|