| 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
|
| Thu, 20 Apr 2023 11:57:34 +0200 |
wenzelm |
clarified signature: explicitly distinguish theory_base_name vs. theory_long_name;
|
file |
diff |
annotate
|
| Mon, 27 Mar 2023 21:48:47 +0200 |
wenzelm |
performance tuning: prefer functor Set() over Table();
|
file |
diff |
annotate
|
| Mon, 20 Sep 2021 23:15:02 +0200 |
wenzelm |
localized command 'syntax' and 'no_syntax';
|
file |
diff |
annotate
|
| Mon, 20 Sep 2021 21:56:10 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Mon, 20 Sep 2021 20:43:38 +0200 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Sat, 04 Sep 2021 21:25:08 +0200 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Thu, 13 May 2021 15:52:10 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Sun, 02 May 2021 17:38:49 +0200 |
wenzelm |
support nested cases;
|
file |
diff |
annotate
|
| Wed, 27 May 2020 20:02:02 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Fri, 03 Apr 2020 17:35:10 +0200 |
wenzelm |
less redundant markup reports;
|
file |
diff |
annotate
|
| Fri, 03 Apr 2020 13:51:56 +0200 |
wenzelm |
more accurate context position reports;
|
file |
diff |
annotate
|
| Thu, 19 Sep 2019 15:09:12 +0200 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Thu, 19 Sep 2019 10:52:18 +0200 |
wenzelm |
clarified modules;
|
file |
diff |
annotate
|
| Wed, 18 Sep 2019 20:53:53 +0200 |
wenzelm |
support soft types for 'assume';
|
file |
diff |
annotate
|
| Wed, 18 Sep 2019 20:10:15 +0200 |
wenzelm |
more robust declaration of resulting statement text, instead of somewhat accidental (Variable.maybe_bind_term result_binds in generic_goal);
|
file |
diff |
annotate
|
| Tue, 17 Sep 2019 17:06:05 +0200 |
wenzelm |
clarified modules;
|
file |
diff |
annotate
|
| Tue, 17 Sep 2019 16:26:57 +0200 |
wenzelm |
clarified signature -- removed unused option (see acb0807ddb56);
|
file |
diff |
annotate
|
| Fri, 09 Aug 2019 17:14:49 +0200 |
wenzelm |
formal position for PThm nodes;
|
file |
diff |
annotate
|
| Sun, 28 Jul 2019 12:11:20 +0200 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Sat, 27 Jul 2019 20:40:00 +0200 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Tue, 16 Jul 2019 15:39:32 +0200 |
wenzelm |
support for a soft-type system within the Isabelle logical framework;
|
file |
diff |
annotate
|
| Mon, 03 Jun 2019 15:40:08 +0200 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Mon, 03 Jun 2019 14:47:27 +0200 |
wenzelm |
tuned whitespace;
|
file |
diff |
annotate
|
| Thu, 09 May 2019 15:47:27 +0200 |
wenzelm |
proper formatting (amending 5076725247fa);
|
file |
diff |
annotate
|
| Thu, 03 Jan 2019 14:12:44 +0100 |
wenzelm |
clarified signature: more types;
|
file |
diff |
annotate
|
| Tue, 27 Nov 2018 21:07:39 +0100 |
wenzelm |
more accurate positions for "name" (quoted string) and "embedded" (cartouche): refer to content without delimiters, which is e.g. relevant for systematic selection/renaming of scope groups;
|
file |
diff |
annotate
|
| Mon, 12 Nov 2018 15:14:12 +0100 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Thu, 25 Oct 2018 15:41:40 +0200 |
wenzelm |
proper completion for @{named_theorems};
|
file |
diff |
annotate
|
| Sun, 23 Sep 2018 21:49:31 +0200 |
wenzelm |
discontinued old-style goal cases;
|
file |
diff |
annotate
|
| Fri, 20 Jul 2018 03:14:44 +0200 |
wenzelm |
added system option "strict_facts";
|
file |
diff |
annotate
|
| Wed, 07 Mar 2018 17:39:18 +0100 |
wenzelm |
tuned -- more uniform;
|
file |
diff |
annotate
|
| Fri, 23 Feb 2018 20:55:46 +0100 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Tue, 20 Feb 2018 16:20:36 +0100 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Mon, 19 Feb 2018 22:07:21 +0100 |
wenzelm |
support for lazy notes in global/local context and Element.Lazy_Notes: name binding and fact without attributes;
|
file |
diff |
annotate
|
| Mon, 19 Feb 2018 18:18:43 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Mon, 19 Feb 2018 14:26:37 +0100 |
wenzelm |
store facts as lazy values;
|
file |
diff |
annotate
|
| Sun, 28 Jan 2018 19:28:52 +0100 |
wenzelm |
clarified take/drop/chop prefix/suffix;
|
file |
diff |
annotate
|
| Mon, 03 Jul 2017 09:20:24 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Mon, 03 Jul 2017 09:12:13 +0200 |
wenzelm |
unused;
|
file |
diff |
annotate
|
| Tue, 13 Dec 2016 11:51:42 +0100 |
wenzelm |
more symbols;
|
file |
diff |
annotate
|
| Tue, 25 Oct 2016 17:22:05 +0200 |
wenzelm |
more robust printing of names in the context of outer syntax;
|
file |
diff |
annotate
|
| Tue, 09 Aug 2016 19:44:28 +0200 |
wenzelm |
print name in parsable form;
|
file |
diff |
annotate
|
| Thu, 04 Aug 2016 21:30:20 +0200 |
wenzelm |
prefer hardwired "nothing";
|
file |
diff |
annotate
|
| Fri, 22 Jul 2016 14:42:32 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Sat, 16 Jul 2016 19:35:27 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Sat, 16 Jul 2016 12:10:37 +0200 |
wenzelm |
re-use name space serial as unique (!) id;
|
file |
diff |
annotate
|
| Sat, 16 Jul 2016 11:32:48 +0200 |
wenzelm |
clarified;
|
file |
diff |
annotate
|
| Sat, 16 Jul 2016 00:38:33 +0200 |
wenzelm |
information about proof outline with cases (sendback);
|
file |
diff |
annotate
|
| Fri, 15 Jul 2016 22:23:36 +0200 |
wenzelm |
unused;
|
file |
diff |
annotate
|
| Tue, 21 Jun 2016 14:42:47 +0200 |
wenzelm |
position information for literal facts;
|
file |
diff |
annotate
|
| Tue, 07 Jun 2016 21:13:08 +0200 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Thu, 12 May 2016 10:03:17 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Tue, 10 May 2016 22:25:06 +0200 |
wenzelm |
find dynamic facts as well, but static ones are preferred;
|
file |
diff |
annotate
|
| Tue, 26 Apr 2016 19:37:47 +0200 |
wenzelm |
more uniform operations for structured statements;
|
file |
diff |
annotate
|
| Tue, 26 Apr 2016 16:20:28 +0200 |
wenzelm |
defs are closed, which leads to proper auto_bind_facts;
|
file |
diff |
annotate
|
| Sun, 24 Apr 2016 20:29:49 +0200 |
wenzelm |
clarified modules;
|
file |
diff |
annotate
|
| Thu, 14 Apr 2016 23:31:10 +0200 |
wenzelm |
highlighting of entity def/ref positions wrt. cursor;
|
file |
diff |
annotate
|
| Tue, 12 Apr 2016 14:50:53 +0200 |
wenzelm |
back to static Mixfix.default_constraint without any special tricks (reverting e6443edaebff);
|
file |
diff |
annotate
|
| Tue, 12 Apr 2016 14:38:57 +0200 |
wenzelm |
Type_Infer.object_logic controls improvement of type inference result;
|
file |
diff |
annotate
|
| Wed, 30 Mar 2016 23:32:50 +0200 |
wenzelm |
more explicit support for object-logic constraint;
|
file |
diff |
annotate
|
| Wed, 30 Mar 2016 21:16:22 +0200 |
wenzelm |
more explicit type;
|
file |
diff |
annotate
|
| Wed, 30 Mar 2016 20:56:39 +0200 |
wenzelm |
relevant check_mixfix happens further at the bottom, to avoid duplicate reports via Specification.prepare;
|
file |
diff |
annotate
|
| Wed, 06 Jan 2016 11:45:07 +0100 |
wenzelm |
more systematic treatment of dynamic facts, when forming closure;
|
file |
diff |
annotate
|
| Tue, 22 Dec 2015 14:20:17 +0100 |
wenzelm |
more accurate lookup of dynamic facts;
|
file |
diff |
annotate
|
| Tue, 08 Dec 2015 10:49:08 +0100 |
wenzelm |
added Proof_Context.add_thms_dynamic, which is potentially useful for Eisbach;
|
file |
diff |
annotate
|
| Fri, 25 Sep 2015 20:37:59 +0200 |
wenzelm |
moved remaining display.ML to more_thm.ML;
|
file |
diff |
annotate
|
| Fri, 25 Sep 2015 19:28:33 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Fri, 25 Sep 2015 19:13:47 +0200 |
wenzelm |
tuned signature: eliminated pointless type Context.pretty;
|
file |
diff |
annotate
|
| Thu, 24 Sep 2015 23:33:29 +0200 |
wenzelm |
more explicit Defs.context: use proper name spaces as far as possible;
|
file |
diff |
annotate
|
| Sun, 13 Sep 2015 22:25:21 +0200 |
wenzelm |
tuned message;
|
file |
diff |
annotate
|
| Thu, 13 Aug 2015 11:05:19 +0200 |
wenzelm |
tuned signature, in accordance to sortBy in Scala;
|
file |
diff |
annotate
|
| Mon, 27 Jul 2015 16:35:12 +0200 |
wenzelm |
tuned signature for print_nested_cases;
|
file |
diff |
annotate
|
| Thu, 02 Jul 2015 12:33:04 +0200 |
wenzelm |
allow to specify suffix of goal parameters;
|
file |
diff |
annotate
|
| Thu, 25 Jun 2015 23:49:05 +0200 |
wenzelm |
implicit goal cases are legacy;
|
file |
diff |
annotate
|
| Thu, 25 Jun 2015 12:10:07 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Wed, 24 Jun 2015 21:26:03 +0200 |
wenzelm |
clarified 'case' command;
|
file |
diff |
annotate
|
| Mon, 15 Jun 2015 16:59:27 +0200 |
wenzelm |
vacuous fact `TERM x`;
|
file |
diff |
annotate
|
| Sun, 14 Jun 2015 15:53:13 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Sun, 14 Jun 2015 14:59:39 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Wed, 10 Jun 2015 11:52:54 +0200 |
wenzelm |
tuned message;
|
file |
diff |
annotate
|
| Tue, 09 Jun 2015 22:24:33 +0200 |
wenzelm |
more uniform treatment of auto bindings vs. explicit user bindings;
|
file |
diff |
annotate
|
| Tue, 09 Jun 2015 16:42:17 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Tue, 09 Jun 2015 11:51:05 +0200 |
wenzelm |
clarified term bindings;
|
file |
diff |
annotate
|
| Mon, 08 Jun 2015 20:53:42 +0200 |
wenzelm |
clarified Proof_Context.cert_propp/read_propp;
|
file |
diff |
annotate
|
| Mon, 08 Jun 2015 19:38:08 +0200 |
wenzelm |
more careful treatment of term bindings in 'obtain' proof body;
|
file |
diff |
annotate
|
| Mon, 08 Jun 2015 14:45:31 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Sun, 07 Jun 2015 23:37:32 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Sun, 07 Jun 2015 22:04:50 +0200 |
wenzelm |
tuned (see also 66e6c539a36d);
|
file |
diff |
annotate
|
| Sun, 07 Jun 2015 21:58:18 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Sun, 07 Jun 2015 21:30:53 +0200 |
wenzelm |
clarified: declare props once and for all;
|
file |
diff |
annotate
|
| Sun, 07 Jun 2015 20:03:40 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Sun, 07 Jun 2015 15:01:07 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Wed, 03 Jun 2015 19:25:05 +0200 |
wenzelm |
clarified context;
|
file |
diff |
annotate
|
| Sun, 03 May 2015 17:19:27 +0200 |
wenzelm |
tuned output -- avoid empty quites and extra breaks;
|
file |
diff |
annotate
|
| Thu, 09 Apr 2015 20:42:32 +0200 |
wenzelm |
clarified keyword 'qualified' in accordance to a similar keyword from Haskell (despite unrelated Binding.qualified in Isabelle/ML);
|
file |
diff |
annotate
|
| Wed, 08 Apr 2015 19:39:08 +0200 |
wenzelm |
proper context for Object_Logic operations;
|
file |
diff |
annotate
|
| Mon, 06 Apr 2015 22:11:01 +0200 |
wenzelm |
support for 'restricted' modifier: only qualified accesses outside the local scope;
|
file |
diff |
annotate
|
| Sat, 04 Apr 2015 14:04:11 +0200 |
wenzelm |
support private scope for individual local theory commands;
|
file |
diff |
annotate
|
| Fri, 03 Apr 2015 19:56:51 +0200 |
wenzelm |
more uniform "verbose" option to print name space;
|
file |
diff |
annotate
|
| Wed, 01 Apr 2015 18:17:44 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Tue, 31 Mar 2015 22:31:05 +0200 |
wenzelm |
support for explicit scope of private entries;
|
file |
diff |
annotate
|
| Tue, 31 Mar 2015 17:34:52 +0200 |
wenzelm |
clarified role of naming for background theory: transform_binding (e.g. for "concealed" flag) uses naming of hypothetical context;
|
file |
diff |
annotate
|
| Tue, 31 Mar 2015 00:11:54 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Sun, 29 Mar 2015 19:23:08 +0200 |
wenzelm |
proper local Proof_Context.arity_sorts;
|
file |
diff |
annotate
|
| Tue, 24 Mar 2015 11:53:18 +0100 |
wenzelm |
clarified input source;
|
file |
diff |
annotate
|
| Fri, 06 Mar 2015 15:58:56 +0100 |
wenzelm |
Thm.cterm_of and Thm.ctyp_of operate on local context;
|
file |
diff |
annotate
|
| Thu, 05 Mar 2015 13:28:04 +0100 |
wenzelm |
tuned -- more explicit use of context;
|
file |
diff |
annotate
|
| Sun, 01 Mar 2015 23:35:41 +0100 |
wenzelm |
added Proof_Context.cterm_of/ctyp_of convenience;
|
file |
diff |
annotate
|
| Fri, 19 Dec 2014 17:23:56 +0100 |
wenzelm |
more frugal Local_Syntax.init -- maintain idents within context;
|
file |
diff |
annotate
|
| Sun, 30 Nov 2014 13:15:04 +0100 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Sun, 30 Nov 2014 12:24:56 +0100 |
wenzelm |
more abstract type Input.source;
|
file |
diff |
annotate
|
| Wed, 26 Nov 2014 20:05:34 +0100 |
wenzelm |
renamed "pairself" to "apply2", in accordance to @{apply 2};
|
file |
diff |
annotate
|
| Sat, 08 Nov 2014 21:31:51 +0100 |
wenzelm |
optional proof context for unify operations, for the sake of proper local options;
|
file |
diff |
annotate
|
| Mon, 13 Oct 2014 22:43:29 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Wed, 20 Aug 2014 11:51:39 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Thu, 14 Aug 2014 16:20:14 +0200 |
wenzelm |
more informative Token.Fact: retain name of dynamic fact (without selection);
|
file |
diff |
annotate
|
| Wed, 13 Aug 2014 14:57:03 +0200 |
wenzelm |
transfer result of Global_Theory.add_thms_dynamic to context stack;
|
file |
diff |
annotate
|
| Sun, 10 Aug 2014 19:44:20 +0200 |
wenzelm |
support aliases within the facts space;
|
file |
diff |
annotate
|