src/Pure/Isar/proof_context.ML
Fri, 17 Sep 2010 20:42:26 +0200 wenzelm simplified some internal flags using Config.T instead of full-blown Proof_Data;
Fri, 17 Sep 2010 20:18:27 +0200 wenzelm tuned signature of (Context_)Position.report variants;
Fri, 17 Sep 2010 17:10:44 +0200 wenzelm allow embedded reports in regular prover messages, to avoid side-effects for errors for example;
Mon, 13 Sep 2010 13:20:18 +0200 wenzelm tuned signature;
Mon, 13 Sep 2010 12:42:08 +0200 wenzelm Type_Infer.finish: index 0 -- freshness supposedly via Name.invents;
Sun, 12 Sep 2010 21:24:23 +0200 wenzelm Type_Infer.infer_types: plain error instead of kernel exception TYPE;
Sun, 12 Sep 2010 20:47:47 +0200 wenzelm load type_infer.ML later -- proper context for Type_Infer.infer_types;
Sun, 12 Sep 2010 19:04:02 +0200 wenzelm eliminated aliases of Type.constraint;
Tue, 07 Sep 2010 16:08:29 +0200 wenzelm highlight bad range of nested error (here from inner parsing);
Mon, 06 Sep 2010 22:31:54 +0200 wenzelm discontinued obsolete ProofContext.prems_limit;
Sun, 05 Sep 2010 22:23:48 +0200 wenzelm Syntax.standard_parse_term: eliminated redundant Pretty.pp;
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;
Thu, 02 Sep 2010 00:48:07 +0200 wenzelm turned show_question_marks into proper configuration option;
Wed, 01 Sep 2010 23:43:45 +0200 wenzelm prefer regular print functions over slightly low-level Term.string_of_vname;
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;
Wed, 11 Aug 2010 15:00:31 +0200 wenzelm tuned whitespace;
Sun, 08 Aug 2010 20:03:31 +0200 wenzelm proper context for Syntax.parse_token;
Sun, 08 Aug 2010 19:54:54 +0200 wenzelm prefer Context_Position.report where a proper context is available -- notably for "inner" entities;
Mon, 31 May 2010 21:06:57 +0200 wenzelm modernized some structure names, keeping a few legacy aliases;
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;
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;
Thu, 29 Apr 2010 22:08:57 +0200 wenzelm read_const: disallow internal names as usual in visible Isar text;
Thu, 29 Apr 2010 16:55:22 +0200 wenzelm ProofContext.read_const: allow for type constraint (for fixed variable);
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;
Wed, 28 Apr 2010 11:41:27 +0200 wenzelm localized default sort;
Wed, 28 Apr 2010 11:13:11 +0200 wenzelm more systematic naming of tsig operations;
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);
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;
Thu, 15 Apr 2010 18:00:21 +0200 wenzelm get_sort: suppress dummyS from input;
Tue, 09 Mar 2010 23:29:04 +0100 wenzelm aliases for class/type/const;
Tue, 09 Mar 2010 14:35:02 +0100 wenzelm added ProofContext.tsig_of -- proforma version for local name space only, not logical content;
Sat, 06 Mar 2010 17:53:04 +0100 wenzelm provide ProofContext.def_type depending on "pattern" mode;
Wed, 03 Mar 2010 00:28:22 +0100 wenzelm authentic syntax for classes and type constructors;
Mon, 01 Mar 2010 17:07:36 +0100 wenzelm more uniform treatment of syntax for types vs. consts;
Sat, 27 Feb 2010 20:51:51 +0100 wenzelm clarified ProofContext.read_const(_proper)/Args.const(_proper) wrt. strict logical consts;
Thu, 25 Feb 2010 22:06:43 +0100 wenzelm clarified ProofContext.read_type_name/Args.type_name wrt strict logical constructors;
Sun, 21 Feb 2010 22:35:02 +0100 wenzelm slightly more abstract syntax mark/unmark operations;
Sun, 21 Feb 2010 21:08:25 +0100 wenzelm authentic syntax for *all* term constants;
Thu, 18 Feb 2010 17:28:02 +0100 berghofe Use top-down rewriting to contract abbreviations.
Tue, 16 Feb 2010 11:59:05 +0100 wenzelm simplified meaning of ProofContext.verbose;
Tue, 16 Feb 2010 11:27:29 +0100 wenzelm misc tuning and simplification;
Mon, 15 Feb 2010 17:17:51 +0100 wenzelm discontinued unnamed infix syntax;
Thu, 11 Feb 2010 22:03:37 +0100 wenzelm added ML antiquotation @{syntax_const};
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
Wed, 25 Nov 2009 09:13:46 +0100 haftmann normalized uncurry take/drop
Tue, 24 Nov 2009 17:28:25 +0100 haftmann curried take/drop
Sun, 15 Nov 2009 19:45:05 +0100 wenzelm eliminated obsolete thm position tags;
Thu, 12 Nov 2009 22:29:54 +0100 wenzelm eliminated slightly odd (unused) "axiom" and "assumption" -- collapsed to unspecific "";
Mon, 09 Nov 2009 20:47:39 +0100 wenzelm locale_const/target_notation: uniform use of Term.aconv_untyped;
Sun, 08 Nov 2009 16:30:41 +0100 wenzelm adapted Generic_Data, Proof_Data;
Mon, 02 Nov 2009 20:48:08 +0100 wenzelm modernized structure Local_Syntax;
Mon, 02 Nov 2009 20:45:23 +0100 wenzelm modernized structure AutoBind;
Mon, 02 Nov 2009 20:30:40 +0100 wenzelm modernized structure Context_Position;
Sun, 01 Nov 2009 15:24:45 +0100 wenzelm modernized structure Rule_Cases;
Tue, 27 Oct 2009 13:24:40 +0100 wenzelm ProofContext.setmp_verbose_CRITICAL;
Sun, 25 Oct 2009 21:35:46 +0100 wenzelm eliminated obsolete tags for types/consts -- now handled via name space, in strongly typed fashion;
Sun, 25 Oct 2009 19:17:42 +0100 wenzelm more direct access to naming;
Sun, 25 Oct 2009 12:27:21 +0100 wenzelm allow name space entries to be "concealed" -- via binding/naming/local_theory;
Sat, 24 Oct 2009 19:47:37 +0200 wenzelm renamed NameSpace to Name_Space -- also to emphasize its subtle change in semantics;
Tue, 20 Oct 2009 21:26:45 +0200 wenzelm backpatching of structure Proof and ProofContext -- avoid odd aliases;
less more (0) -300 -100 -60 tip