| Tue, 15 May 2018 17:07:41 +0200 |
wenzelm |
more uniform output (cf. 450cefec7c11);
|
file |
diff |
annotate
|
| Sat, 17 Feb 2018 12:58:07 +0100 |
wenzelm |
more informative theories_trace;
|
file |
diff |
annotate
|
| Fri, 16 Feb 2018 14:11:25 +0100 |
wenzelm |
optional trace of created theory values;
|
file |
diff |
annotate
|
| Thu, 15 Feb 2018 17:08:25 +0100 |
wenzelm |
auxiliary operation for space profiling;
|
file |
diff |
annotate
|
| Fri, 18 Aug 2017 13:55:05 +0200 |
wenzelm |
more informative error message, e.g. relevant for incoherent imports;
|
file |
diff |
annotate
|
| Mon, 10 Apr 2017 22:59:29 +0200 |
wenzelm |
proper display_name;
|
file |
diff |
annotate
|
| Mon, 10 Apr 2017 21:43:21 +0200 |
wenzelm |
clarified theory_long_name (for qualified access to Thy_Info) vs. short theory_name (which is unique within any given theory context);
|
file |
diff |
annotate
|
| Wed, 06 Apr 2016 16:33:33 +0200 |
wenzelm |
clarified modules;
|
file |
diff |
annotate
|
| Tue, 05 Apr 2016 20:03:24 +0200 |
wenzelm |
clarified modules -- simplified bootstrap;
|
file |
diff |
annotate
|
| Sat, 02 Apr 2016 21:10:07 +0200 |
wenzelm |
careful export of type-dependent functions, without losing their special status;
|
file |
diff |
annotate
|
| Fri, 18 Mar 2016 16:26:35 +0100 |
wenzelm |
clarified modules;
|
file |
diff |
annotate
|
| Sun, 20 Dec 2015 13:11:47 +0100 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Sun, 20 Dec 2015 13:06:26 +0100 |
wenzelm |
renamed Pretty.str_of to Pretty.unformatted_string_of to emphasize its meaning;
|
file |
diff |
annotate
|
| Fri, 25 Sep 2015 20:04:25 +0200 |
wenzelm |
less redundant output;
|
file |
diff |
annotate
|
| Fri, 25 Sep 2015 19:13:47 +0200 |
wenzelm |
tuned signature: eliminated pointless type Context.pretty;
|
file |
diff |
annotate
|
| Mon, 31 Aug 2015 14:16:32 +0200 |
wenzelm |
tuned message;
|
file |
diff |
annotate
|
| Sun, 30 Aug 2015 15:21:25 +0200 |
wenzelm |
clarified exceptions;
|
file |
diff |
annotate
|
| Fri, 28 Aug 2015 23:48:03 +0200 |
wenzelm |
clarified exceptions: avoid interference of formal context failure with regular rule application failure (which is routinely handled in user-space);
|
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
|
| Sun, 16 Aug 2015 17:11:31 +0200 |
wenzelm |
separate type theory_id;
|
file |
diff |
annotate
|
| Sat, 20 Dec 2014 19:12:41 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Thu, 18 Dec 2014 15:21:54 +0100 |
wenzelm |
avoid repeated access to global variable (101 times in Complex_Main), which is actually synchronized after e557a9ddee5f;
|
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, 17 Feb 2014 22:39:20 +0100 |
wenzelm |
subtle change of semantics of Thm.eq_thm, e.g. relevant for merge of src/HOL/Tools/Predicate_Compile/core_data.ML (cf. HOL-IMP);
|
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
|
| Wed, 17 Jul 2013 09:32:08 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Wed, 10 Apr 2013 17:02:47 +0200 |
wenzelm |
added ML antiquotation @{theory_context};
|
file |
diff |
annotate
|
| Thu, 07 Mar 2013 15:02:55 +0100 |
wenzelm |
tuned signature -- prefer terminology of Scala and Axiom;
|
file |
diff |
annotate
|
| Sat, 08 Dec 2012 13:25:49 +0100 |
wenzelm |
check consistent theory names for direct imports as well -- as claimed in the comments (see also 1cc36c0ec9eb);
|
file |
diff |
annotate
|
| Wed, 29 Aug 2012 11:48:45 +0200 |
wenzelm |
renamed Position.str_of to Position.here;
|
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
|
| Wed, 06 Jul 2011 20:46:06 +0200 |
wenzelm |
prefer Synchronized.var;
|
file |
diff |
annotate
|
| Thu, 30 Jun 2011 16:50:26 +0200 |
wenzelm |
back to sequential merge_data, reverting 741373421318 (NB: expensive Parser.merge_gram is already asynchronous since 3daff3cc2214);
|
file |
diff |
annotate
|
| Sun, 15 May 2011 20:38:08 +0200 |
wenzelm |
timing of Theory_Data operations, with implicit thread positions when functor is applied;
|
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 15:47:52 +0200 |
wenzelm |
modernized structure Proof_Context;
|
file |
diff |
annotate
|
| Sat, 05 Feb 2011 20:38:32 +0100 |
wenzelm |
more tracing information via Par_List.map_name;
|
file |
diff |
annotate
|
| Wed, 01 Sep 2010 15:33:59 +0200 |
haftmann |
replaced Table.map' by Table.map
|
file |
diff |
annotate
|
| Wed, 21 Jul 2010 15:31:38 +0200 |
wenzelm |
replaced Thy_Info.the_theory by Context.this_theory -- avoid referring to accidental theory loader state;
|
file |
diff |
annotate
|
| Wed, 21 Jul 2010 14:27:05 +0200 |
wenzelm |
added Context.get_theory -- avoid referring to accidental theory loader state (cf. Thy_Info.get_theory);
|
file |
diff |
annotate
|
| Tue, 20 Jul 2010 14:44:33 +0200 |
wenzelm |
eliminated old-style sys_error/SYS_ERROR in favour of exception Fail -- after careful checking that there is no overlap with existing handling of that;
|
file |
diff |
annotate
|
| Mon, 31 May 2010 21:06:57 +0200 |
wenzelm |
modernized some structure names, keeping a few legacy aliases;
|
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
|
| Mon, 04 Jan 2010 23:20:35 +0100 |
wenzelm |
discontinued old TheoryDataFun, but retain Theory_Data_PP with is Pretty.pp argument to merge (still required in exotic situations -- hard to get rid of);
|
file |
diff |
annotate
|
| Mon, 04 Jan 2010 20:25:56 +0100 |
wenzelm |
removed further remains of mutable theory data (cf. 25bd3ed2ac9f);
|
file |
diff |
annotate
|
| Mon, 04 Jan 2010 14:09:56 +0100 |
haftmann |
dropped copy operation for legacy TheoryDataFun
|
file |
diff |
annotate
|
| Wed, 11 Nov 2009 00:11:26 +0100 |
wenzelm |
local mutex for theory content/identity operations;
|
file |
diff |
annotate
|
| Sun, 08 Nov 2009 16:27:50 +0100 |
wenzelm |
modernized/simplified functor Theory_Data, Proof_Data, Generic_Data: eliminated Pretty.pp, discontinued mutable data;
|
file |
diff |
annotate
|
| Tue, 20 Oct 2009 22:46:24 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Tue, 20 Oct 2009 21:26:45 +0200 |
wenzelm |
backpatching of structure Proof and ProofContext -- avoid odd aliases;
|
file |
diff |
annotate
|
| Wed, 30 Sep 2009 22:20:58 +0200 |
wenzelm |
eliminated redundant bindings;
|
file |
diff |
annotate
|
| Tue, 29 Sep 2009 11:49:22 +0200 |
wenzelm |
explicit indication of Unsynchronized.ref;
|
file |
diff |
annotate
|
| Thu, 09 Jul 2009 22:01:41 +0200 |
wenzelm |
renamed functor TableFun to Table, and GraphFun to Graph;
|
file |
diff |
annotate
|
| Sat, 21 Mar 2009 20:00:23 +0100 |
wenzelm |
removed obsolete pprint operations;
|
file |
diff |
annotate
|
| Tue, 06 Jan 2009 14:43:35 +0100 |
wenzelm |
renamed structure ParList to Par_List;
|
file |
diff |
annotate
|
| Tue, 06 Jan 2009 14:33:49 +0100 |
wenzelm |
parallelized merge_data;
|
file |
diff |
annotate
|
| Sat, 13 Dec 2008 15:35:18 +0100 |
wenzelm |
tuned comments;
|
file |
diff |
annotate
|
| Sat, 13 Dec 2008 15:06:24 +0100 |
wenzelm |
refined identity and ancestry: explicit draft flat, ids are unnamed, name consistency is checked for ancestry;
|
file |
diff |
annotate
|
| Thu, 11 Dec 2008 20:31:45 +0100 |
wenzelm |
unified ids for ancestors and checkpoints, removed obsolete history of checkpoints;
|
file |
diff |
annotate
|
| Sat, 06 Dec 2008 00:08:07 +0100 |
wenzelm |
finish_thy: to not collapse checkpoints -- allows future proofs to be deferred indefinitely (performance tradeoff: 5-15% slowdown in sequential batch jobs);
|
file |
diff |
annotate
|
| Thu, 16 Oct 2008 22:44:26 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Fri, 26 Sep 2008 19:07:56 +0200 |
wenzelm |
eliminated polymorphic equality;
|
file |
diff |
annotate
|
| Mon, 22 Sep 2008 15:26:11 +0200 |
wenzelm |
added reject_draft;
|
file |
diff |
annotate
|
| Thu, 04 Sep 2008 16:03:44 +0200 |
wenzelm |
Thread.getLocal/setLocal;
|
file |
diff |
annotate
|
| Tue, 24 Jun 2008 19:43:17 +0200 |
wenzelm |
added pprint_thy_ref;
|
file |
diff |
annotate
|
| Sun, 18 May 2008 17:03:20 +0200 |
wenzelm |
eliminated theory CPure;
|
file |
diff |
annotate
|
| Wed, 14 May 2008 14:43:37 +0200 |
wenzelm |
names_of: exclude intermediate ids -- less verbosity;
|
file |
diff |
annotate
|
| Thu, 10 Apr 2008 20:54:15 +0200 |
wenzelm |
export is_draft, not draftN;
|
file |
diff |
annotate
|
| Sat, 29 Mar 2008 19:14:08 +0100 |
wenzelm |
added map_theory_result, map_proof_result;
|
file |
diff |
annotate
|
| Fri, 28 Mar 2008 20:02:04 +0100 |
wenzelm |
Context.>> : operate on Context.generic;
|
file |
diff |
annotate
|
| Thu, 27 Mar 2008 15:32:15 +0100 |
wenzelm |
eliminated delayed theory setup
|
file |
diff |
annotate
|
| Thu, 27 Mar 2008 14:41:14 +0100 |
wenzelm |
eliminated theory ProtoPure;
|
file |
diff |
annotate
|
| Thu, 27 Mar 2008 12:06:26 +0100 |
wenzelm |
nonfix >>;
|
file |
diff |
annotate
|
| Wed, 26 Mar 2008 22:40:03 +0100 |
wenzelm |
added thread data (formerly global ref in ML/ml_context.ML);
|
file |
diff |
annotate
|
| Sat, 08 Sep 2007 19:58:35 +0200 |
wenzelm |
removed thy_ord (erratic due to multi-threading);
|
file |
diff |
annotate
|
| Mon, 20 Aug 2007 23:41:35 +0200 |
wenzelm |
tuned CRITICAL sections;
|
file |
diff |
annotate
|
| Wed, 08 Aug 2007 16:40:20 +0200 |
wenzelm |
thread-safeness: when creating certified items, perform Theory.check_thy *last*;
|
file |
diff |
annotate
|
| Fri, 03 Aug 2007 16:28:20 +0200 |
wenzelm |
improved check_thy: produce a checked theory_ref (thread-safe version);
|
file |
diff |
annotate
|
| Mon, 23 Jul 2007 20:47:56 +0200 |
wenzelm |
marked some CRITICAL sections;
|
file |
diff |
annotate
|
| Thu, 05 Jul 2007 20:01:32 +0200 |
wenzelm |
the_theory/proof: error instead of exception Fail;
|
file |
diff |
annotate
|
| Wed, 13 Jun 2007 00:01:58 +0200 |
wenzelm |
merge/merge_refs: plain error instead of exception TERM;
|
file |
diff |
annotate
|
| Mon, 07 May 2007 00:50:09 +0200 |
wenzelm |
simplified DataFun interfaces: removed name/print, use adhoc value for uninitialized data, init only required for impure data;
|
file |
diff |
annotate
|
| Mon, 30 Apr 2007 13:33:00 +0200 |
wenzelm |
removed obsolete get_sg;
|
file |
diff |
annotate
|
| Thu, 05 Apr 2007 00:30:31 +0200 |
wenzelm |
added thy_ord -- order of creation;
|
file |
diff |
annotate
|
| Wed, 04 Apr 2007 23:29:39 +0200 |
wenzelm |
theory: maintain ancestors in order of creation;
|
file |
diff |
annotate
|
| Sun, 21 Jan 2007 16:46:06 +0100 |
wenzelm |
*** MESSAGE REFERS TO PREVIOUS VERSION ***
|
file |
diff |
annotate
|
| Sun, 21 Jan 2007 16:43:47 +0100 |
wenzelm |
tuned comments
|
file |
diff |
annotate
|
| Sat, 20 Jan 2007 14:09:16 +0100 |
wenzelm |
added is_finished_thy;
|
file |
diff |
annotate
|
| Fri, 19 Jan 2007 22:08:02 +0100 |
wenzelm |
moved ML context stuff to from Context to ML_Context;
|
file |
diff |
annotate
|
| Fri, 19 Jan 2007 13:09:32 +0100 |
wenzelm |
ML context: full generic context, tuned signature;
|
file |
diff |
annotate
|
| Sat, 30 Dec 2006 16:08:00 +0100 |
wenzelm |
removed conditional combinator;
|
file |
diff |
annotate
|
| Tue, 05 Dec 2006 22:14:45 +0100 |
wenzelm |
added mapping_result;
|
file |
diff |
annotate
|
| Fri, 24 Nov 2006 22:05:14 +0100 |
wenzelm |
fake predeclaration of structure ProofContext;
|
file |
diff |
annotate
|
| Mon, 09 Oct 2006 19:37:05 +0200 |
wenzelm |
moved Context.ml_output to Output.ml_output;
|
file |
diff |
annotate
|
| Sun, 01 Oct 2006 22:19:24 +0200 |
wenzelm |
exists_name: include this theory name;
|
file |
diff |
annotate
|
| Wed, 02 Aug 2006 22:26:51 +0200 |
wenzelm |
fake predeclaration of type Proof.context;
|
file |
diff |
annotate
|
| Wed, 07 Jun 2006 16:53:31 +0200 |
haftmann |
fixed typo
|
file |
diff |
annotate
|
| Wed, 17 May 2006 22:34:47 +0200 |
wenzelm |
added mapping;
|
file |
diff |
annotate
|
| Thu, 27 Apr 2006 15:06:35 +0200 |
wenzelm |
tuned basic list operators (flat, maps, map_filter);
|
file |
diff |
annotate
|
| Wed, 15 Feb 2006 21:34:55 +0100 |
wenzelm |
removed distinct, renamed gen_distinct to distinct;
|
file |
diff |
annotate
|
| Sun, 12 Feb 2006 21:34:22 +0100 |
wenzelm |
structure Datatab: private copy avoids potential conflict of table exceptions;
|
file |
diff |
annotate
|
| Mon, 06 Feb 2006 20:58:57 +0100 |
wenzelm |
TableFun: renamed xxx_multi to xxx_list;
|
file |
diff |
annotate
|
| Sat, 21 Jan 2006 23:02:23 +0100 |
wenzelm |
rename map_theory/proof to theory/proof_map;
|
file |
diff |
annotate
|
| Thu, 19 Jan 2006 21:22:16 +0100 |
wenzelm |
setup: theory -> theory;
|
file |
diff |
annotate
|
| Sat, 14 Jan 2006 17:14:06 +0100 |
wenzelm |
sane ERROR handling;
|
file |
diff |
annotate
|
| Fri, 13 Jan 2006 01:13:02 +0100 |
wenzelm |
added map_theory, map_proof;
|
file |
diff |
annotate
|
| Tue, 10 Jan 2006 19:33:31 +0100 |
wenzelm |
support for generic contexts with data;
|
file |
diff |
annotate
|
| Tue, 04 Oct 2005 19:01:37 +0200 |
wenzelm |
minor tweaks for Poplog/ML;
|
file |
diff |
annotate
|
| Thu, 15 Sep 2005 17:16:56 +0200 |
wenzelm |
TableFun/Symtab: curried lookup and update;
|
file |
diff |
annotate
|
| Tue, 13 Sep 2005 22:19:24 +0200 |
wenzelm |
replaced DATA_FAIL by EXCEPTION;
|
file |
diff |
annotate
|
| Thu, 01 Sep 2005 18:48:50 +0200 |
wenzelm |
curried_lookup/update;
|
file |
diff |
annotate
|
| Tue, 16 Aug 2005 13:42:31 +0200 |
wenzelm |
type proof: theory_ref instead of theory (make proof contexts independent entities);
|
file |
diff |
annotate
|
| Tue, 19 Jul 2005 20:47:01 +0200 |
wenzelm |
Inttab.defined;
|
file |
diff |
annotate
|
| Wed, 06 Jul 2005 20:00:24 +0200 |
wenzelm |
check_thy: less invocations, less verbose;
|
file |
diff |
annotate
|
| Wed, 29 Jun 2005 15:13:23 +0200 |
wenzelm |
added joinable;
|
file |
diff |
annotate
|
| Wed, 22 Jun 2005 19:41:18 +0200 |
wenzelm |
begin_thy: merge maximal imports;
|
file |
diff |
annotate
|
| Mon, 20 Jun 2005 22:14:03 +0200 |
wenzelm |
improved treatment of intermediate checkpoints: actual copy
|
file |
diff |
annotate
|