src/Pure/global_theory.ML
Sun, 28 Jul 2019 14:37:32 +0200 wenzelm tuned;
Sun, 28 Jul 2019 14:28:40 +0200 wenzelm clarified signature;
Sun, 28 Jul 2019 12:35:59 +0200 wenzelm tuned;
Sun, 28 Jul 2019 12:11:20 +0200 wenzelm clarified signature;
Sun, 28 Jul 2019 11:53:51 +0200 wenzelm tuned;
Sat, 27 Jul 2019 21:47:43 +0200 wenzelm tuned;
Sat, 27 Jul 2019 20:40:00 +0200 wenzelm clarified signature;
Sat, 28 Jul 2018 16:50:55 +0200 wenzelm more robust: do not defer potentially slow/big lazy facts to the very end;
Sat, 28 Jul 2018 16:30:58 +0200 wenzelm tuned;
Fri, 20 Jul 2018 03:14:44 +0200 wenzelm added system option "strict_facts";
Sun, 01 Jul 2018 12:38:37 +0200 wenzelm discontinued pending_shyps: too much complication due to lazy facts;
Fri, 29 Jun 2018 15:54:41 +0200 wenzelm disallow pending hyps;
Sun, 20 May 2018 22:37:00 +0200 wenzelm more checks for global facts: disallow undeclared frees (as in Export_Theory.export_fact);
Wed, 07 Mar 2018 17:39:18 +0100 wenzelm tuned -- more uniform;
Fri, 23 Feb 2018 21:27:20 +0100 wenzelm tuned signature;
Fri, 23 Feb 2018 20:55:46 +0100 wenzelm tuned signature;
Tue, 20 Feb 2018 16:20:14 +0100 wenzelm tuned;
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;
Mon, 19 Feb 2018 14:30:06 +0100 wenzelm tuned: more accurate transfer;
Mon, 19 Feb 2018 14:26:37 +0100 wenzelm store facts as lazy values;
Mon, 10 Apr 2017 21:05:31 +0200 wenzelm tuned signature;
Wed, 13 Jan 2016 17:05:08 +0100 wenzelm tuned;
Wed, 13 Jan 2016 16:55:56 +0100 wenzelm removed old 'defs' command;
Fri, 25 Sep 2015 19:13:47 +0200 wenzelm tuned signature: eliminated pointless type Context.pretty;
Thu, 24 Sep 2015 23:33:29 +0200 wenzelm more explicit Defs.context: use proper name spaces as far as possible;
Sun, 30 Aug 2015 17:34:29 +0200 wenzelm trim context for persistent storage;
Thu, 14 Aug 2014 16:20:14 +0200 wenzelm more informative Token.Fact: retain name of dynamic fact (without selection);
Wed, 13 Aug 2014 16:06:32 +0200 wenzelm tuned signature -- proper Local_Theory.add_thms_dynamic;
Sun, 10 Aug 2014 19:44:20 +0200 wenzelm support aliases within the facts space;
Sat, 15 Mar 2014 11:59:18 +0100 wenzelm tuned signature;
Fri, 14 Mar 2014 10:08:36 +0100 wenzelm just one cumulative Proof_Context.facts, with uniform retrieval (including PIDE markup, completion etc.);
Sun, 09 Mar 2014 17:02:18 +0100 wenzelm check fact names with PIDE markup;
Tue, 25 Feb 2014 11:36:04 +0100 wenzelm more positions;
Tue, 30 Jul 2013 15:09:25 +0200 wenzelm type theory is purely value-oriented;
Sun, 25 Nov 2012 19:49:24 +0100 wenzelm Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
Tue, 09 Oct 2012 19:24:19 +0200 wenzelm more explicit flags for facts table;
Sat, 01 Sep 2012 19:43:18 +0200 wenzelm discontinued complicated/unreliable notion of recent proofs within context;
Fri, 31 Aug 2012 22:24:14 +0200 wenzelm tuned signature;
Thu, 30 Aug 2012 19:18:49 +0200 wenzelm some support for registering forked proofs within Proof.state, using its bottom context;
Thu, 30 Aug 2012 16:39:50 +0200 wenzelm tuned signature;
Wed, 29 Aug 2012 11:48:45 +0200 wenzelm renamed Position.str_of to Position.here;
Wed, 04 Apr 2012 17:14:19 +0200 wenzelm tuned comments;
Sun, 18 Mar 2012 13:51:51 +0100 wenzelm tuned;
Sun, 18 Mar 2012 13:04:22 +0100 wenzelm maintain generic context naming in structure Name_Space (NB: empty = default_naming, init = local_naming);
Sat, 03 Mar 2012 21:43:59 +0100 wenzelm canonical argument order for attribute application;
Mon, 28 Nov 2011 22:05:32 +0100 wenzelm separate module for concrete Isabelle markup;
Sat, 26 Nov 2011 14:14:51 +0100 wenzelm memoing of forked proofs;
Fri, 19 Aug 2011 23:25:47 +0200 wenzelm maintain recent future proofs at transaction boundaries;
Sat, 23 Apr 2011 19:41:53 +0200 wenzelm hardwired mapping "_" -> "Pure.asm_rl" avoids legacy binding;
Sun, 17 Apr 2011 21:42:47 +0200 wenzelm added Binding.print convenience, which includes quote already;
Sun, 17 Apr 2011 21:04:22 +0200 wenzelm tuned signature;
Sun, 17 Apr 2011 20:58:43 +0200 wenzelm markup facts via name space;
Sun, 17 Apr 2011 20:15:46 +0200 wenzelm eliminated obsolete markup -- superseded by generic "entity" markup;
Sun, 17 Apr 2011 19:54:04 +0200 wenzelm report Name_Space.declare/define, relatively to context;
Wed, 02 Feb 2011 22:48:24 +0100 wenzelm tuned odd conditional expression;
Mon, 20 Sep 2010 16:05:25 +0200 wenzelm renamed structure PureThy to Pure_Thy and moved most content to Global_Theory, to emphasize that this is global-only;
less more (0) tip