| Mon, 08 Jan 2024 21:54:20 +0100 |
wenzelm |
minor performance tuning;
|
file |
diff |
annotate
|
| Sun, 31 Dec 2023 22:04:41 +0100 |
wenzelm |
minor performance tuning: proper Same.operation;
|
file |
diff |
annotate
|
| Fri, 22 Dec 2023 21:03:16 +0100 |
wenzelm |
clarified signature: downgrade old-style Global_Theory.add_defs to Global_Theory.add_def without attributes;
|
file |
diff |
annotate
|
| Wed, 20 Dec 2023 22:32:57 +0100 |
wenzelm |
proper Thm.transfer;
|
file |
diff |
annotate
|
| Sat, 22 Apr 2023 21:00:24 +0200 |
wenzelm |
tuned: concise combinators instead of bulky case-expressions;
|
file |
diff |
annotate
|
| Thu, 20 Apr 2023 21:26:35 +0200 |
wenzelm |
support n-ary merge theory data;
|
file |
diff |
annotate
|
| Wed, 20 Oct 2021 18:13:17 +0200 |
wenzelm |
discontinued obsolete "val extend = I" for data slots;
|
file |
diff |
annotate
|
| Tue, 06 Aug 2019 19:47:46 +0200 |
wenzelm |
backed out changeset 1b8858f4c393: odd problems e.g. in CAVA_LTL_Modelchecker;
|
file |
diff |
annotate
|
| Mon, 05 Aug 2019 16:11:43 +0200 |
wenzelm |
clarified modules: more direct data implementation;
|
file |
diff |
annotate
|
| Fri, 02 Aug 2019 11:23:09 +0200 |
wenzelm |
clarified modules: inference kernel maintains sort algebra within the logic;
|
file |
diff |
annotate
|
| Thu, 01 Aug 2019 14:46:50 +0200 |
wenzelm |
more elementary treatment of standard_vars (unconstrainT is already standard);
|
file |
diff |
annotate
|
| Sun, 21 Jul 2019 12:28:02 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Fri, 16 Feb 2018 18:55:42 +0100 |
wenzelm |
removed unused material;
|
file |
diff |
annotate
|
| Fri, 16 Feb 2018 18:29:11 +0100 |
wenzelm |
trim context of persistent data;
|
file |
diff |
annotate
|
| Mon, 09 May 2016 14:37:47 +0200 |
wenzelm |
clarified context, notably for internal use of Simplifier;
|
file |
diff |
annotate
|
| Thu, 07 Apr 2016 12:08:02 +0200 |
wenzelm |
prefer regular context update, to allow continuous editing of Pure;
|
file |
diff |
annotate
|
| Fri, 25 Sep 2015 19:13:47 +0200 |
wenzelm |
tuned signature: eliminated pointless type Context.pretty;
|
file |
diff |
annotate
|
| Tue, 22 Sep 2015 22:42:48 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Tue, 22 Sep 2015 22:38:22 +0200 |
wenzelm |
eliminated separate type Theory.dep: use typeargs uniformly for consts/types;
|
file |
diff |
annotate
|
| Tue, 22 Sep 2015 15:58:19 +0200 |
wenzelm |
tuned whitespace;
|
file |
diff |
annotate
|
| Tue, 22 Sep 2015 14:32:23 +0200 |
wenzelm |
HOL typedef with explicit dependency checks according to Ondrey Kuncar, 07-Jul-2015, 16-Jul-2015, 30-Jul-2015;
|
file |
diff |
annotate
|
| Mon, 27 Jul 2015 17:44:55 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Tue, 31 Mar 2015 00:11:54 +0200 |
wenzelm |
tuned signature;
|
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
|
| Wed, 04 Mar 2015 19:53:18 +0100 |
wenzelm |
tuned signature -- prefer qualified names;
|
file |
diff |
annotate
|
| Mon, 23 Feb 2015 14:50:30 +0100 |
wenzelm |
Goal.prove_multi is superseded by the fully general Goal.prove_common;
|
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, 12 May 2014 17:17:32 +0200 |
wenzelm |
tuned signature to make axiomatizations more easy to spot in the source, via "add_axioms" or "axiomatization";
|
file |
diff |
annotate
|
| Fri, 14 Mar 2014 15:12:22 +0100 |
wenzelm |
conceal somewhat obscure internal facts, e.g. relevant for 'print_theorems', 'find_theorems';
|
file |
diff |
annotate
|
| Mon, 10 Feb 2014 22:08:18 +0100 |
wenzelm |
discontinued axiomatic 'classes', 'classrel', 'arities';
|
file |
diff |
annotate
|