| Sat, 17 Mar 2012 23:55:03 +0100 |
proper naming of simprocs according to actual target context;
|
file | diff | annotate |
| Wed, 14 Mar 2012 17:52:38 +0100 |
source positions for locale and class expressions;
|
file | diff | annotate |
| Fri, 09 Mar 2012 20:04:19 +0100 |
tuned signature;
|
file | diff | annotate |
| Sat, 03 Mar 2012 21:43:59 +0100 |
canonical argument order for attribute application;
|
file | diff | annotate |
| Mon, 28 Nov 2011 22:05:32 +0100 |
separate module for concrete Isabelle markup;
|
file | diff | annotate |
| Sun, 27 Nov 2011 21:53:38 +0100 |
tuned;
|
file | diff | annotate |
| Fri, 11 Nov 2011 12:52:57 +0100 |
more scalable Proof_Context.prepare_sorts;
|
file | diff | annotate |
| Wed, 09 Nov 2011 20:47:11 +0100 |
tuned signature;
|
file | diff | annotate |
| Wed, 09 Nov 2011 17:57:42 +0100 |
sort assignment before simultaneous term_check, not isolated parse_term;
|
file | diff | annotate |
| Thu, 03 Nov 2011 23:55:53 +0100 |
more general Proof_Context.bind_propp, which allows outer parameters;
|
file | diff | annotate |
| Thu, 03 Nov 2011 22:23:41 +0100 |
tuned signature -- canonical argument order;
|
file | diff | annotate |
| Wed, 13 Jul 2011 20:36:18 +0200 |
sub-structural sharing after Syntax.check phase, with global interning of logical entities (the latter is relevant when bypassing default parsing via YXML);
|
file | diff | annotate |
| Sat, 25 Jun 2011 19:38:35 +0200 |
entity markup for "type", "constant";
|
file | diff | annotate |
| Sat, 25 Jun 2011 18:15:36 +0200 |
type classes: entity markup instead of old-style token markup;
|
file | diff | annotate |
| Thu, 12 May 2011 16:23:13 +0200 |
proper configuration options Proof_Context.debug and Proof_Context.verbose;
|
file | diff | annotate |
| Thu, 28 Apr 2011 21:06:04 +0200 |
literal facts `prop` may contain dummy patterns;
|
file | diff | annotate |
| Thu, 28 Apr 2011 20:20:49 +0200 |
eliminated slightly odd Proof_Context.bind_fixes;
|
file | diff | annotate |
| Wed, 27 Apr 2011 23:02:43 +0200 |
more precise positions via binding;
|
file | diff | annotate |
| Wed, 27 Apr 2011 20:58:40 +0200 |
tuned signature -- eliminated odd comment;
|
file | diff | annotate |
| Wed, 27 Apr 2011 20:19:05 +0200 |
more precise position information via Variable.add_fixes_binding;
|
file | diff | annotate |
| Wed, 27 Apr 2011 17:58:45 +0200 |
reorganized fixes as specialized (global) name space;
|
file | diff | annotate |
| Sat, 23 Apr 2011 18:46:01 +0200 |
clarified Consts.read_const;
|
file | diff | annotate |
| Sat, 23 Apr 2011 18:25:50 +0200 |
clarified Type.the_decl;
|
file | diff | annotate |
| Sat, 23 Apr 2011 18:09:27 +0200 |
more reports and error positions;
|
file | diff | annotate |
| Tue, 19 Apr 2011 20:47:02 +0200 |
split Type_Infer into early and late part, after Proof_Context;
|
file | diff | annotate |
| Tue, 19 Apr 2011 14:57:09 +0200 |
simplified check/uncheck interfaces: result comparison is hardwired by default;
|
file | diff | annotate |
| Mon, 18 Apr 2011 13:26:39 +0200 |
pass plain Proof.context for pretty printing;
|
file | diff | annotate |
| Mon, 18 Apr 2011 11:13:29 +0200 |
simplified pretty printing context, which is only required for certain kernel operations;
|
file | diff | annotate |
| Sun, 17 Apr 2011 21:42:47 +0200 |
added Binding.print convenience, which includes quote already;
|
file | diff | annotate |
| Sun, 17 Apr 2011 21:04:22 +0200 |
tuned signature;
|
file | diff | annotate |
| Sun, 17 Apr 2011 20:58:43 +0200 |
markup facts via name space;
|
file | diff | annotate |
| Sun, 17 Apr 2011 20:15:46 +0200 |
eliminated obsolete markup -- superseded by generic "entity" markup;
|
file | diff | annotate |
| Sun, 17 Apr 2011 19:54:04 +0200 |
report Name_Space.declare/define, relatively to context;
|
file | diff | annotate |
| Sat, 16 Apr 2011 16:37:21 +0200 |
do not open ML structures;
|
file | diff | annotate |
| Sat, 16 Apr 2011 15:47:52 +0200 |
modernized structure Proof_Context;
|
file | diff | annotate |
| Sat, 16 Apr 2011 15:25:25 +0200 |
prefer local name spaces;
|
file | diff | annotate |
| Sat, 16 Apr 2011 13:48:45 +0200 |
Name_Space: proper configuration options long_names, short_names, unique_names instead of former unsynchronized references;
|
file | diff | annotate |
| Sat, 16 Apr 2011 12:46:18 +0200 |
tuned signature, disentangled dependencies;
|
file | diff | annotate |
| Fri, 08 Apr 2011 20:39:09 +0200 |
moved CONST syntax/translations to their proper place;
|
file | diff | annotate |
| Fri, 08 Apr 2011 16:34:14 +0200 |
discontinued special treatment of structure Lexicon;
|
file | diff | annotate |
| Fri, 08 Apr 2011 14:20:57 +0200 |
discontinued special treatment of structure Mixfix;
|
file | diff | annotate |
| Thu, 07 Apr 2011 17:52:44 +0200 |
simplified printer context: uniform externing and static token translations;
|
file | diff | annotate |
| Wed, 06 Apr 2011 15:10:39 +0200 |
eliminated odd object-oriented type_context/term_context;
|
file | diff | annotate |
| Tue, 05 Apr 2011 23:14:41 +0200 |
moved decode/parse operations to standard_syntax.ML;
|
file | diff | annotate |
| Tue, 05 Apr 2011 18:06:45 +0200 |
separate module for standard implementation of inner syntax operations;
|
file | diff | annotate |
| Tue, 05 Apr 2011 14:25:18 +0200 |
discontinued special treatment of structure Ast: no pervasive content, no inclusion in structure Syntax;
|
file | diff | annotate |
| Tue, 05 Apr 2011 13:07:40 +0200 |
more precise propagation of reports/results through some inner syntax layers;
|
file | diff | annotate |
| Sun, 03 Apr 2011 21:59:33 +0200 |
added Position.reports convenience;
|
file | diff | annotate |
| Wed, 30 Mar 2011 22:53:18 +0200 |
accomodate autofix discipline of non-body context;
|
file | diff | annotate |
| Wed, 30 Mar 2011 22:03:50 +0200 |
more informative markup_free;
|
file | diff | annotate |
| Sun, 27 Mar 2011 20:55:01 +0200 |
decode_term: some context-sensitive markup;
|
file | diff | annotate |
| Sun, 27 Mar 2011 19:51:51 +0200 |
tuned signatures;
|
file | diff | annotate |
| Sun, 27 Mar 2011 17:55:11 +0200 |
decode_term/disambig: report resolved term variables for the unique (!) result;
|
file | diff | annotate |
| Sat, 04 Dec 2010 18:41:12 +0100 |
added Syntax.default_root;
|
file | diff | annotate |
| Thu, 02 Dec 2010 16:52:52 +0100 |
configuration option "show_abbrevs" supersedes print mode "no_abbrevs", with inverted meaning;
|
file | diff | annotate |
| Mon, 20 Sep 2010 16:05:25 +0200 |
renamed structure PureThy to Pure_Thy and moved most content to Global_Theory, to emphasize that this is global-only;
|
file | diff | annotate |
| Fri, 17 Sep 2010 20:42:26 +0200 |
simplified some internal flags using Config.T instead of full-blown Proof_Data;
|
file | diff | annotate |
| Fri, 17 Sep 2010 20:18:27 +0200 |
tuned signature of (Context_)Position.report variants;
|
file | diff | annotate |
| Fri, 17 Sep 2010 17:10:44 +0200 |
allow embedded reports in regular prover messages, to avoid side-effects for errors for example;
|
file | diff | annotate |
| Mon, 13 Sep 2010 13:20:18 +0200 |
tuned signature;
|
file | diff | annotate |