| Wed, 10 Jan 2024 14:36:29 +0100 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Wed, 10 Jan 2024 13:24:59 +0100 |
wenzelm |
clarified test: no exception yet;
|
file |
diff |
annotate
|
| Wed, 10 Jan 2024 13:18:28 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Wed, 10 Jan 2024 13:16:48 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Wed, 10 Jan 2024 13:15:28 +0100 |
wenzelm |
tuned signature: more direct operations;
|
file |
diff |
annotate
|
| Wed, 10 Jan 2024 13:10:20 +0100 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Wed, 10 Jan 2024 11:39:01 +0100 |
wenzelm |
clarified signature: more direct operations;
|
file |
diff |
annotate
|
| Wed, 10 Jan 2024 11:33:36 +0100 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Wed, 10 Jan 2024 11:28:20 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Tue, 09 Jan 2024 23:52:02 +0100 |
wenzelm |
minor performance tuning, for important special case where consts are already expanded (e.g. re-certification within proof procedure);
|
file |
diff |
annotate
|
| Tue, 09 Jan 2024 23:41:50 +0100 |
wenzelm |
tuned whitespace;
|
file |
diff |
annotate
|
| Tue, 09 Jan 2024 23:40:53 +0100 |
wenzelm |
more robust: certify types uniformly (see also 62b75508eb66);
|
file |
diff |
annotate
|
| Tue, 09 Jan 2024 23:38:54 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Tue, 09 Jan 2024 22:40:38 +0100 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Tue, 09 Jan 2024 17:10:09 +0100 |
wenzelm |
misc tuning and clarification: prefer Same.operation;
|
file |
diff |
annotate
|
| Tue, 09 Jan 2024 16:04:21 +0100 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Tue, 09 Jan 2024 12:18:01 +0100 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Sat, 06 May 2023 23:20:20 +0200 |
wenzelm |
back to more elementary concept of aliases as adhoc change of accesses, but now with "suppress" information (see also 31ea5c1f874d);
|
file |
diff |
annotate
|
| Fri, 05 May 2023 15:56:12 +0200 |
wenzelm |
more explicit entries for aliases, with proper checks in "strict" mode (e.g. for logical entities);
|
file |
diff |
annotate
|
| Sat, 11 Sep 2021 21:16:23 +0200 |
wenzelm |
ML antiquotations for type constructors and term constants;
|
file |
diff |
annotate
|
| Thu, 09 Sep 2021 12:33:14 +0200 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Sat, 04 Sep 2021 21:25:08 +0200 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Fri, 03 Sep 2021 18:57:33 +0200 |
wenzelm |
more scalable data structure (but: rarely used many arguments);
|
file |
diff |
annotate
|
| Fri, 04 Oct 2019 16:25:45 +0200 |
wenzelm |
proper replacement for (map_types (K dummyT));
|
file |
diff |
annotate
|
| Mon, 08 Aug 2016 21:26:00 +0200 |
wenzelm |
Item_Net.retrieve_matching requires beta-eta normal form (amending 8976c5bc9e97);
|
file |
diff |
annotate
|
| Mon, 01 Aug 2016 11:54:32 +0200 |
wenzelm |
more restrictive retrieval of rules for matching instead of unification -- relevant for performance of printing terms;
|
file |
diff |
annotate
|
| Fri, 25 Sep 2015 19:13:47 +0200 |
wenzelm |
tuned signature: eliminated pointless type Context.pretty;
|
file |
diff |
annotate
|
| Thu, 13 Mar 2014 17:26:22 +0100 |
wenzelm |
more frugal recording of changes: join merely requires information from one side;
|
file |
diff |
annotate
|
| Wed, 12 Mar 2014 14:37:14 +0100 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Tue, 11 Mar 2014 22:49:28 +0100 |
wenzelm |
more efficient local theory operations, by imposing a linear change discipline on the main types/consts tables, in order to speed-up Proof_Context.transfer_syntax required for Local_Theory.raw_theory_result;
|
file |
diff |
annotate
|
| Mon, 10 Mar 2014 13:55:03 +0100 |
wenzelm |
abstract type Name_Space.table;
|
file |
diff |
annotate
|
| Sun, 09 Mar 2014 17:43:40 +0100 |
wenzelm |
unused;
|
file |
diff |
annotate
|
| Thu, 06 Mar 2014 16:12:26 +0100 |
wenzelm |
reject internal term names outright, and complete consts instead;
|
file |
diff |
annotate
|
| Thu, 06 Mar 2014 11:32:16 +0100 |
wenzelm |
clarified treatment of consts -- prefer value-oriented reports;
|
file |
diff |
annotate
|
| Sun, 02 Mar 2014 21:30:47 +0100 |
wenzelm |
prefer Name_Space.check with its builtin reports (including completion);
|
file |
diff |
annotate
|
| Tue, 08 Jan 2013 12:39:39 +0100 |
wenzelm |
tuned -- prefer high-level Table.merge with its slightly more conservative update;
|
file |
diff |
annotate
|
| Sun, 25 Nov 2012 19:49:24 +0100 |
wenzelm |
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
|
file |
diff |
annotate
|
| Wed, 29 Aug 2012 11:48:45 +0200 |
wenzelm |
renamed Position.str_of to Position.here;
|
file |
diff |
annotate
|
| Sun, 18 Mar 2012 13:04:22 +0100 |
wenzelm |
maintain generic context naming in structure Name_Space (NB: empty = default_naming, init = local_naming);
|
file |
diff |
annotate
|
| Mon, 28 Nov 2011 22:05:32 +0100 |
wenzelm |
separate module for concrete Isabelle markup;
|
file |
diff |
annotate
|
| Wed, 13 Jul 2011 20:36:18 +0200 |
wenzelm |
sub-structural sharing after Syntax.check phase, with global interning of logical entities (the latter is relevant when bypassing default parsing via YXML);
|
file |
diff |
annotate
|
| Sat, 25 Jun 2011 19:38:35 +0200 |
wenzelm |
entity markup for "type", "constant";
|
file |
diff |
annotate
|
| Sat, 23 Apr 2011 18:46:01 +0200 |
wenzelm |
clarified Consts.read_const;
|
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
|
| Sun, 17 Apr 2011 21:42:47 +0200 |
wenzelm |
added Binding.print convenience, which includes quote already;
|
file |
diff |
annotate
|
| Sun, 17 Apr 2011 19:54:04 +0200 |
wenzelm |
report Name_Space.declare/define, relatively to context;
|
file |
diff |
annotate
|
| Sat, 16 Apr 2011 13:48:45 +0200 |
wenzelm |
Name_Space: proper configuration options long_names, short_names, unique_names instead of former unsynchronized references;
|
file |
diff |
annotate
|
| Fri, 08 Apr 2011 16:34:14 +0200 |
wenzelm |
discontinued special treatment of structure Lexicon;
|
file |
diff |
annotate
|
| Thu, 24 Mar 2011 16:56:19 +0100 |
wenzelm |
added Term.is_open and Term.is_dependent convenience, to cover common situations of loose bounds;
|
file |
diff |
annotate
|
| Fri, 17 Dec 2010 22:23:56 +0100 |
wenzelm |
extra checking of name bindings for classes, types, consts;
|
file |
diff |
annotate
|
| Fri, 26 Nov 2010 22:29:41 +0100 |
wenzelm |
make two copies (!) of Library.UnequalLengths coincide with ListPair.UnequalLengths;
|
file |
diff |
annotate
|
| Thu, 27 May 2010 18:10:37 +0200 |
wenzelm |
renamed structure PrintMode to Print_Mode, keeping the old name as legacy alias for some time;
|
file |
diff |
annotate
|
| Tue, 09 Mar 2010 23:29:04 +0100 |
wenzelm |
aliases for class/type/const;
|
file |
diff |
annotate
|
| Wed, 03 Mar 2010 22:50:35 +0100 |
wenzelm |
added extern_syntax;
|
file |
diff |
annotate
|
| Sun, 21 Feb 2010 22:35:02 +0100 |
wenzelm |
slightly more abstract syntax mark/unmark operations;
|
file |
diff |
annotate
|
| Sun, 21 Feb 2010 21:08:25 +0100 |
wenzelm |
authentic syntax for *all* term constants;
|
file |
diff |
annotate
|
| Sun, 01 Nov 2009 20:59:34 +0100 |
wenzelm |
adapted Item_Net;
|
file |
diff |
annotate
|
| Sun, 25 Oct 2009 21:35:46 +0100 |
wenzelm |
eliminated obsolete tags for types/consts -- now handled via name space, in strongly typed fashion;
|
file |
diff |
annotate
|
| Sun, 25 Oct 2009 13:18:35 +0100 |
wenzelm |
conceal consts via name space, not tags;
|
file |
diff |
annotate
|
| Sat, 24 Oct 2009 21:30:33 +0200 |
wenzelm |
maintain position of formal entities via name space;
|
file |
diff |
annotate
|