src/Pure/global_theory.ML
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