| Sun, 03 Apr 2011 21:59:33 +0200 |
wenzelm |
added Position.reports convenience;
|
file |
diff |
annotate
|
| Wed, 30 Mar 2011 22:53:18 +0200 |
wenzelm |
accomodate autofix discipline of non-body context;
|
file |
diff |
annotate
|
| Wed, 30 Mar 2011 22:03:50 +0200 |
wenzelm |
more informative markup_free;
|
file |
diff |
annotate
|
| Sun, 27 Mar 2011 20:55:01 +0200 |
wenzelm |
decode_term: some context-sensitive markup;
|
file |
diff |
annotate
|
| Sun, 27 Mar 2011 19:51:51 +0200 |
wenzelm |
tuned signatures;
|
file |
diff |
annotate
|
| Sun, 27 Mar 2011 17:55:11 +0200 |
wenzelm |
decode_term/disambig: report resolved term variables for the unique (!) result;
|
file |
diff |
annotate
|
| Sat, 04 Dec 2010 18:41:12 +0100 |
wenzelm |
added Syntax.default_root;
|
file |
diff |
annotate
|
| Thu, 02 Dec 2010 16:52:52 +0100 |
wenzelm |
configuration option "show_abbrevs" supersedes print mode "no_abbrevs", with inverted meaning;
|
file |
diff |
annotate
|
| 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;
|
file |
diff |
annotate
|
| Fri, 17 Sep 2010 20:42:26 +0200 |
wenzelm |
simplified some internal flags using Config.T instead of full-blown Proof_Data;
|
file |
diff |
annotate
|
| Fri, 17 Sep 2010 20:18:27 +0200 |
wenzelm |
tuned signature of (Context_)Position.report variants;
|
file |
diff |
annotate
|
| Fri, 17 Sep 2010 17:10:44 +0200 |
wenzelm |
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 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Mon, 13 Sep 2010 12:42:08 +0200 |
wenzelm |
Type_Infer.finish: index 0 -- freshness supposedly via Name.invents;
|
file |
diff |
annotate
|
| Sun, 12 Sep 2010 21:24:23 +0200 |
wenzelm |
Type_Infer.infer_types: plain error instead of kernel exception TYPE;
|
file |
diff |
annotate
|
| Sun, 12 Sep 2010 20:47:47 +0200 |
wenzelm |
load type_infer.ML later -- proper context for Type_Infer.infer_types;
|
file |
diff |
annotate
|
| Sun, 12 Sep 2010 19:04:02 +0200 |
wenzelm |
eliminated aliases of Type.constraint;
|
file |
diff |
annotate
|
| Tue, 07 Sep 2010 16:08:29 +0200 |
wenzelm |
highlight bad range of nested error (here from inner parsing);
|
file |
diff |
annotate
|
| Mon, 06 Sep 2010 22:31:54 +0200 |
wenzelm |
discontinued obsolete ProofContext.prems_limit;
|
file |
diff |
annotate
|
| Sun, 05 Sep 2010 22:23:48 +0200 |
wenzelm |
Syntax.standard_parse_term: eliminated redundant Pretty.pp;
|
file |
diff |
annotate
|
| Thu, 02 Sep 2010 23:45:37 +0200 |
wenzelm |
inner parsing: refrain from too many nested position reports to achieve more precise error feedback in the source;
|
file |
diff |
annotate
|
| Thu, 02 Sep 2010 00:48:07 +0200 |
wenzelm |
turned show_question_marks into proper configuration option;
|
file |
diff |
annotate
|
| Wed, 01 Sep 2010 23:43:45 +0200 |
wenzelm |
prefer regular print functions over slightly low-level Term.string_of_vname;
|
file |
diff |
annotate
|
| Thu, 26 Aug 2010 13:09:12 +0200 |
wenzelm |
renamed ProofContext.theory(_result) to ProofContext.background_theory(_result) to emphasize that this belongs to the infrastructure and is rarely appropriate in user-space tools;
|
file |
diff |
annotate
|
| Wed, 11 Aug 2010 15:00:31 +0200 |
wenzelm |
tuned whitespace;
|
file |
diff |
annotate
|
| Sun, 08 Aug 2010 20:03:31 +0200 |
wenzelm |
proper context for Syntax.parse_token;
|
file |
diff |
annotate
|
| Sun, 08 Aug 2010 19:54:54 +0200 |
wenzelm |
prefer Context_Position.report where a proper context is available -- notably for "inner" entities;
|
file |
diff |
annotate
|
| Mon, 31 May 2010 21:06:57 +0200 |
wenzelm |
modernized some structure names, keeping a few legacy aliases;
|
file |
diff |
annotate
|
| Thu, 27 May 2010 17:41:27 +0200 |
wenzelm |
renamed structure TypeInfer to Type_Infer, keeping the old name as legacy alias for some time;
|
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
|
| Thu, 29 Apr 2010 22:08:57 +0200 |
wenzelm |
read_const: disallow internal names as usual in visible Isar text;
|
file |
diff |
annotate
|
| Thu, 29 Apr 2010 16:55:22 +0200 |
wenzelm |
ProofContext.read_const: allow for type constraint (for fixed variable);
|
file |
diff |
annotate
|
| Thu, 29 Apr 2010 11:05:13 +0200 |
wenzelm |
allow mixfix syntax for fixes within a proof body -- should now work thanks to fully authentic syntax;
|
file |
diff |
annotate
|
| Wed, 28 Apr 2010 11:41:27 +0200 |
wenzelm |
localized default sort;
|
file |
diff |
annotate
|
| Wed, 28 Apr 2010 11:13:11 +0200 |
wenzelm |
more systematic naming of tsig operations;
|
file |
diff |
annotate
|
| Wed, 28 Apr 2010 10:51:34 +0200 |
wenzelm |
get_sort: minimize sorts given in the text, while keeping those from the context unchanged (the latter are preferred);
|
file |
diff |
annotate
|
| Tue, 27 Apr 2010 21:46:10 +0200 |
wenzelm |
monotonic sort certification: sorts are no longer minimized at the kernel boundary, only when reading input from the end-user;
|
file |
diff |
annotate
|
| Thu, 15 Apr 2010 18:00:21 +0200 |
wenzelm |
get_sort: suppress dummyS from input;
|
file |
diff |
annotate
|
| Tue, 09 Mar 2010 23:29:04 +0100 |
wenzelm |
aliases for class/type/const;
|
file |
diff |
annotate
|
| Tue, 09 Mar 2010 14:35:02 +0100 |
wenzelm |
added ProofContext.tsig_of -- proforma version for local name space only, not logical content;
|
file |
diff |
annotate
|
| Sat, 06 Mar 2010 17:53:04 +0100 |
wenzelm |
provide ProofContext.def_type depending on "pattern" mode;
|
file |
diff |
annotate
|
| Wed, 03 Mar 2010 00:28:22 +0100 |
wenzelm |
authentic syntax for classes and type constructors;
|
file |
diff |
annotate
|
| Mon, 01 Mar 2010 17:07:36 +0100 |
wenzelm |
more uniform treatment of syntax for types vs. consts;
|
file |
diff |
annotate
|
| Sat, 27 Feb 2010 20:51:51 +0100 |
wenzelm |
clarified ProofContext.read_const(_proper)/Args.const(_proper) wrt. strict logical consts;
|
file |
diff |
annotate
|
| Thu, 25 Feb 2010 22:06:43 +0100 |
wenzelm |
clarified ProofContext.read_type_name/Args.type_name wrt strict logical constructors;
|
file |
diff |
annotate
|
| Sun, 21 Feb 2010 22:35:02 +0100 |
wenzelm |
slightly more abstract syntax mark/unmark operations;
|
file |
diff |
annotate
|
| Sun, 21 Feb 2010 21:08:25 +0100 |
wenzelm |
authentic syntax for *all* term constants;
|
file |
diff |
annotate
|
| Thu, 18 Feb 2010 17:28:02 +0100 |
berghofe |
Use top-down rewriting to contract abbreviations.
|
file |
diff |
annotate
|
| Tue, 16 Feb 2010 11:59:05 +0100 |
wenzelm |
simplified meaning of ProofContext.verbose;
|
file |
diff |
annotate
|
| Tue, 16 Feb 2010 11:27:29 +0100 |
wenzelm |
misc tuning and simplification;
|
file |
diff |
annotate
|
| Mon, 15 Feb 2010 17:17:51 +0100 |
wenzelm |
discontinued unnamed infix syntax;
|
file |
diff |
annotate
|
| Thu, 11 Feb 2010 22:03:37 +0100 |
wenzelm |
added ML antiquotation @{syntax_const};
|
file |
diff |
annotate
|
| Tue, 02 Feb 2010 11:38:38 +0100 |
blanchet |
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
|
file |
diff |
annotate
|
| Wed, 25 Nov 2009 09:13:46 +0100 |
haftmann |
normalized uncurry take/drop
|
file |
diff |
annotate
|
| Tue, 24 Nov 2009 17:28:25 +0100 |
haftmann |
curried take/drop
|
file |
diff |
annotate
|
| Sun, 15 Nov 2009 19:45:05 +0100 |
wenzelm |
eliminated obsolete thm position tags;
|
file |
diff |
annotate
|
| Thu, 12 Nov 2009 22:29:54 +0100 |
wenzelm |
eliminated slightly odd (unused) "axiom" and "assumption" -- collapsed to unspecific "";
|
file |
diff |
annotate
|
| Mon, 09 Nov 2009 20:47:39 +0100 |
wenzelm |
locale_const/target_notation: uniform use of Term.aconv_untyped;
|
file |
diff |
annotate
|
| Sun, 08 Nov 2009 16:30:41 +0100 |
wenzelm |
adapted Generic_Data, Proof_Data;
|
file |
diff |
annotate
|
| Mon, 02 Nov 2009 20:48:08 +0100 |
wenzelm |
modernized structure Local_Syntax;
|
file |
diff |
annotate
|