| Fri, 17 Jul 2020 14:56:55 +0200 |
wenzelm |
prefer conservative extend/merge of theory naming;
|
file |
diff |
annotate
|
| Fri, 03 Apr 2020 13:51:56 +0200 |
wenzelm |
more accurate context position reports;
|
file |
diff |
annotate
|
| Sat, 23 Nov 2019 14:48:44 +0100 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Tue, 22 Oct 2019 20:55:13 +0200 |
wenzelm |
clarified axiom_table: uniform space (e.g. like consts), e.g. relevant for export of HOL-ex.Join_Theory;
|
file |
diff |
annotate
|
| Thu, 04 Jul 2019 14:20:47 +0200 |
wenzelm |
proper theory naming after join (reset due to merge_data);
|
file |
diff |
annotate
|
| Thu, 04 Jul 2019 12:31:24 +0200 |
wenzelm |
support join of anonymous theory nodes, e.g. relevant for parallel theory construction;
|
file |
diff |
annotate
|
| Sat, 09 Mar 2019 23:57:07 +0100 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Mon, 12 Nov 2018 15:14:12 +0100 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Fri, 22 Jun 2018 20:31:49 +0200 |
wenzelm |
clarified document antiquotation @{theory};
|
file |
diff |
annotate
|
| Thu, 21 Jun 2018 14:49:21 +0200 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Sun, 13 May 2018 15:05:31 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Tue, 09 Jan 2018 14:07:39 +0100 |
wenzelm |
clarified exception;
|
file |
diff |
annotate
|
| Mon, 08 Jan 2018 22:36:02 +0100 |
wenzelm |
clarified implicit Pure.thy;
|
file |
diff |
annotate
|
| Wed, 19 Apr 2017 12:27:36 +0200 |
wenzelm |
proper base name, e.g. relevant for Code_Namespace.hierarchical_program;
|
file |
diff |
annotate
|
| Mon, 07 Nov 2016 19:07:30 +0100 |
wenzelm |
unused since 15865e0c5598;
|
file |
diff |
annotate
|
| Tue, 05 Jul 2016 14:20:27 +0200 |
wenzelm |
PIDE reports of implicit variable scope;
|
file |
diff |
annotate
|
| Mon, 25 Apr 2016 17:37:36 +0200 |
wenzelm |
more rigid check of lhs;
|
file |
diff |
annotate
|
| Sun, 24 Apr 2016 20:37:24 +0200 |
wenzelm |
within a proof body context, undeclared frees are like global constants;
|
file |
diff |
annotate
|
| Mon, 28 Dec 2015 16:29:39 +0100 |
wenzelm |
suppress irrelevant position reports;
|
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
|
| 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 16:49:56 +0200 |
wenzelm |
renamed Defs.node to Defs.item;
|
file |
diff |
annotate
|
| Tue, 22 Sep 2015 16:17:49 +0200 |
wenzelm |
tuned signature;
|
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
|
| Fri, 28 Aug 2015 23:21:04 +0200 |
wenzelm |
more abstract theory certificate, which is not necessarily the full theory;
|
file |
diff |
annotate
|
| Sun, 16 Aug 2015 18:19:30 +0200 |
wenzelm |
prefer theory_id operations;
|
file |
diff |
annotate
|
| Thu, 16 Apr 2015 17:18:48 +0200 |
wenzelm |
formal Theory.check, with markup and completion;
|
file |
diff |
annotate
|
| Mon, 06 Apr 2015 12:51:25 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Fri, 07 Nov 2014 22:15:51 +0100 |
wenzelm |
eliminated pointless check -- command definitions are subject to theory context;
|
file |
diff |
annotate
|
| Tue, 14 Oct 2014 10:52:46 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Fri, 04 Jul 2014 17:41:35 +0200 |
wenzelm |
insist in explicit overloading;
|
file |
diff |
annotate
|
| Wed, 12 Mar 2014 10:42:28 +0100 |
wenzelm |
more explicit Sign.change_check -- detect structural mistakes where they emerge, not at later theory merges;
|
file |
diff |
annotate
|
| Mon, 10 Mar 2014 13:55:03 +0100 |
wenzelm |
abstract type Name_Space.table;
|
file |
diff |
annotate
|
| Fri, 23 Aug 2013 20:35:50 +0200 |
wenzelm |
added Theory.setup convenience;
|
file |
diff |
annotate
|
| Tue, 30 Jul 2013 15:09:25 +0200 |
wenzelm |
type theory is purely value-oriented;
|
file |
diff |
annotate
|
| Thu, 18 Jul 2013 13:12:54 +0200 |
wenzelm |
immutable theory values with full stamp record of every update (increase of stamp size for HOL: 20000 -> 100000, JinjaThreads: 65000 -> 300000) -- minimal measurable impact on inference kernel performance;
|
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
|
| Sun, 26 Aug 2012 22:23:10 +0200 |
wenzelm |
entity markup for theory Pure, to enable hyperlinks etc.;
|
file |
diff |
annotate
|
| Sun, 26 Aug 2012 21:46:50 +0200 |
wenzelm |
theory def/ref position reports, which enable hyperlinks etc.;
|
file |
diff |
annotate
|
| Wed, 01 Aug 2012 19:53:20 +0200 |
wenzelm |
more standard bootstrapping of Pure.thy;
|
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
|
| Fri, 16 Mar 2012 22:48:38 +0100 |
wenzelm |
eliminated odd 'finalconsts' / Theory.add_finals;
|
file |
diff |
annotate
|
| Fri, 25 Nov 2011 16:32:29 +0100 |
wenzelm |
prefer Parser.make_gram over Parser.merge_gram, to approximate n-ary merges on theory import;
|
file |
diff |
annotate
|
| Wed, 07 Sep 2011 21:05:53 +0200 |
wenzelm |
explicit join_syntax ensures command transaction integrity of 'theory';
|
file |
diff |
annotate
|
| Wed, 20 Apr 2011 13:54:07 +0200 |
wenzelm |
added Theory.nodes_of convenience;
|
file |
diff |
annotate
|
| Mon, 18 Apr 2011 15:01:50 +0200 |
wenzelm |
recovered Theory.check_def: full name needs to be determined from background thy, not auxiliary ctxt (broken in 774df7c59508, caused Nitpick.all_axioms_of to produce bad results);
|
file |
diff |
annotate
|
| Mon, 18 Apr 2011 14:05:39 +0200 |
wenzelm |
pass plain Proof.context for pretty printing;
|
file |
diff |
annotate
|
| Mon, 18 Apr 2011 11:44:39 +0200 |
wenzelm |
pass plain Proof.context for pretty printing;
|
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 15:47:52 +0200 |
wenzelm |
modernized structure Proof_Context;
|
file |
diff |
annotate
|
| Sun, 20 Mar 2011 22:47:08 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Sun, 05 Sep 2010 21:41:24 +0200 |
wenzelm |
turned show_sorts/show_types into proper configuration options;
|
file |
diff |
annotate
|
| Sun, 05 Sep 2010 19:47:40 +0200 |
wenzelm |
pretty printing: prefer regular Proof.context over Pretty.pp, which is mostly for special bootstrap purposes involving theory merge, for example;
|
file |
diff |
annotate
|
| Mon, 03 May 2010 14:25:56 +0200 |
wenzelm |
renamed ProofContext.init to ProofContext.init_global to emphasize that this is not the real thing;
|
file |
diff |
annotate
|
| Sat, 27 Mar 2010 17:36:32 +0100 |
wenzelm |
disallow premises in primitive Theory.add_def -- handle in Thm.add_def;
|
file |
diff |
annotate
|