src/Pure/Isar/proof_context.ML
Wed, 29 May 2013 18:25:11 +0200 wenzelm tuned signature -- more explicit flags for low-level Thm.bicompose;
Sun, 26 May 2013 19:27:32 +0200 wenzelm tuned signature;
Wed, 10 Apr 2013 17:02:47 +0200 wenzelm added ML antiquotation @{theory_context};
Wed, 03 Apr 2013 13:58:00 +0200 wenzelm tuned output -- less bullets;
Sat, 30 Mar 2013 13:40:19 +0100 wenzelm more item markup;
Sat, 30 Mar 2013 12:13:39 +0100 wenzelm item markup for Proof_Context.pretty_fact;
Mon, 26 Nov 2012 21:46:04 +0100 wenzelm tuned signature;
Sun, 25 Nov 2012 19:49:24 +0100 wenzelm Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
Mon, 19 Nov 2012 20:23:47 +0100 wenzelm theorem status about oracles/futures is no longer printed by default;
Wed, 17 Oct 2012 10:46:14 +0200 wenzelm more formal markup;
Tue, 09 Oct 2012 19:24:19 +0200 wenzelm more explicit flags for facts table;
Wed, 03 Oct 2012 17:12:08 +0200 wenzelm more error positions;
Wed, 03 Oct 2012 14:58:56 +0200 wenzelm allow position constraints to coexist with 0 or 1 sort constraints;
Mon, 01 Oct 2012 16:37:22 +0200 wenzelm report sort assignment of visible type variables;
Wed, 29 Aug 2012 11:48:45 +0200 wenzelm renamed Position.str_of to Position.here;
Mon, 02 Apr 2012 19:47:21 +0200 wenzelm tuned signature;
Sun, 01 Apr 2012 18:01:19 +0200 wenzelm tuned signature;
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, 17 Mar 2012 23:55:03 +0100 wenzelm proper naming of simprocs according to actual target context;
Wed, 14 Mar 2012 17:52:38 +0100 wenzelm source positions for locale and class expressions;
Fri, 09 Mar 2012 20:04:19 +0100 wenzelm tuned signature;
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;
Sun, 27 Nov 2011 21:53:38 +0100 wenzelm tuned;
Fri, 11 Nov 2011 12:52:57 +0100 wenzelm more scalable Proof_Context.prepare_sorts;
Wed, 09 Nov 2011 20:47:11 +0100 wenzelm tuned signature;
Wed, 09 Nov 2011 17:57:42 +0100 wenzelm sort assignment before simultaneous term_check, not isolated parse_term;
Thu, 03 Nov 2011 23:55:53 +0100 wenzelm more general Proof_Context.bind_propp, which allows outer parameters;
Thu, 03 Nov 2011 22:23:41 +0100 wenzelm tuned signature -- canonical argument order;
Wed, 13 Jul 2011 20:36:18 +0200 wenzelm sub-structural sharing after Syntax.check phase, with global interning of logical entities (the latter is relevant when bypassing default parsing via YXML);
Sat, 25 Jun 2011 19:38:35 +0200 wenzelm entity markup for "type", "constant";
Sat, 25 Jun 2011 18:15:36 +0200 wenzelm type classes: entity markup instead of old-style token markup;
Thu, 12 May 2011 16:23:13 +0200 wenzelm proper configuration options Proof_Context.debug and Proof_Context.verbose;
Thu, 28 Apr 2011 21:06:04 +0200 wenzelm literal facts `prop` may contain dummy patterns;
Thu, 28 Apr 2011 20:20:49 +0200 wenzelm eliminated slightly odd Proof_Context.bind_fixes;
Wed, 27 Apr 2011 23:02:43 +0200 wenzelm more precise positions via binding;
Wed, 27 Apr 2011 20:58:40 +0200 wenzelm tuned signature -- eliminated odd comment;
Wed, 27 Apr 2011 20:19:05 +0200 wenzelm more precise position information via Variable.add_fixes_binding;
Wed, 27 Apr 2011 17:58:45 +0200 wenzelm reorganized fixes as specialized (global) name space;
Sat, 23 Apr 2011 18:46:01 +0200 wenzelm clarified Consts.read_const;
Sat, 23 Apr 2011 18:25:50 +0200 wenzelm clarified Type.the_decl;
Sat, 23 Apr 2011 18:09:27 +0200 wenzelm more reports and error positions;
Tue, 19 Apr 2011 20:47:02 +0200 wenzelm split Type_Infer into early and late part, after Proof_Context;
Tue, 19 Apr 2011 14:57:09 +0200 wenzelm simplified check/uncheck interfaces: result comparison is hardwired by default;
Mon, 18 Apr 2011 13:26:39 +0200 wenzelm pass plain Proof.context for pretty printing;
Mon, 18 Apr 2011 11:13:29 +0200 wenzelm simplified pretty printing context, which is only required for certain kernel operations;
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;
Sat, 16 Apr 2011 16:37:21 +0200 wenzelm do not open ML structures;
Sat, 16 Apr 2011 15:47:52 +0200 wenzelm modernized structure Proof_Context;
Sat, 16 Apr 2011 15:25:25 +0200 wenzelm prefer local name spaces;
Sat, 16 Apr 2011 13:48:45 +0200 wenzelm Name_Space: proper configuration options long_names, short_names, unique_names instead of former unsynchronized references;
Sat, 16 Apr 2011 12:46:18 +0200 wenzelm tuned signature, disentangled dependencies;
Fri, 08 Apr 2011 20:39:09 +0200 wenzelm moved CONST syntax/translations to their proper place;
Fri, 08 Apr 2011 16:34:14 +0200 wenzelm discontinued special treatment of structure Lexicon;
Fri, 08 Apr 2011 14:20:57 +0200 wenzelm discontinued special treatment of structure Mixfix;
Thu, 07 Apr 2011 17:52:44 +0200 wenzelm simplified printer context: uniform externing and static token translations;
less more (0) -300 -100 -60 tip