src/Pure/Proof/proof_syntax.ML
Fri, 08 Nov 2019 20:12:57 +0100 wenzelm retain type information from reconstruct_proof, notably for Export_Theory.export_thm;
Fri, 08 Nov 2019 19:06:50 +0100 wenzelm clarified modules;
Sun, 03 Nov 2019 15:45:46 +0100 wenzelm clarified signature -- more options;
Fri, 01 Nov 2019 15:23:23 +0100 wenzelm clarified modules (again);
Fri, 01 Nov 2019 15:09:55 +0100 wenzelm more detailed proof term output;
Sun, 20 Oct 2019 20:38:22 +0200 wenzelm clarified expand_proof/expand_name: allow more detailed control via thm_header;
Sun, 20 Oct 2019 16:16:23 +0200 wenzelm option to export standardized proof terms (not scalable);
Fri, 11 Oct 2019 21:51:10 +0200 wenzelm clarified standard_proof_of: prefer expand_proof over somewhat adhoc strip_thm_proof;
Wed, 09 Oct 2019 22:22:17 +0200 wenzelm tuned;
Fri, 09 Aug 2019 15:58:26 +0200 wenzelm clarified ML types;
Tue, 30 Jul 2019 20:09:25 +0200 wenzelm clarified global theory context;
Tue, 30 Jul 2019 14:35:29 +0200 wenzelm clarified modules: provide reconstruct_proof / expand_proof at the bottom of proof term construction;
Tue, 30 Jul 2019 11:41:39 +0200 wenzelm clarified modules;
Fri, 26 Jul 2019 15:21:02 +0200 wenzelm proper argument type (amending 42fbb6abed5a);
Fri, 26 Jul 2019 14:43:56 +0200 wenzelm tuned signature;
Fri, 26 Jul 2019 09:35:02 +0200 wenzelm defer rew_proof on unnamed PThm node as open_proof operation: significant performance improvement;
Wed, 24 Jul 2019 13:18:15 +0200 wenzelm clarified syntax;
Mon, 22 Jul 2019 11:09:24 +0200 wenzelm unused (see also 42fbb6abed5a);
Sun, 21 Jul 2019 15:42:43 +0200 wenzelm discontinued ASCII syntax;
Sun, 21 Jul 2019 15:19:07 +0200 wenzelm global declaration of abstract syntax for proof terms, with qualified names;
Sun, 21 Jul 2019 12:28:02 +0200 wenzelm tuned;
Sun, 18 Feb 2018 15:05:21 +0100 wenzelm tuned signature;
Sat, 04 Feb 2017 21:15:11 +0100 wenzelm more uniform use of Reconstruct.clean_proof_of;
Tue, 13 Dec 2016 11:51:42 +0100 wenzelm more symbols;
Tue, 12 Apr 2016 14:38:57 +0200 wenzelm Type_Infer.object_logic controls improvement of type inference result;
Sat, 09 Apr 2016 13:28:32 +0200 wenzelm clarified context;
Wed, 30 Mar 2016 15:15:12 +0200 wenzelm clarified simple mixfix;
Tue, 29 Mar 2016 21:17:29 +0200 wenzelm more position information for type mixfix;
Tue, 29 Dec 2015 14:58:15 +0100 wenzelm former "xsymbols" syntax is used by default, and ASCII replacement syntax with print mode "ASCII";
Tue, 28 Jul 2015 23:14:40 +0200 wenzelm clarified context;
Fri, 06 Mar 2015 15:58:56 +0100 wenzelm Thm.cterm_of and Thm.ctyp_of operate on local context;
Wed, 04 Mar 2015 19:53:18 +0100 wenzelm tuned signature -- prefer qualified names;
Sun, 06 Apr 2014 15:43:45 +0200 wenzelm more source positions;
Fri, 21 Mar 2014 12:34:50 +0100 wenzelm more qualified names;
Fri, 21 Mar 2014 11:42:32 +0100 wenzelm more qualified names;
Fri, 21 Mar 2014 11:06:39 +0100 wenzelm tuned signature;
Fri, 21 Mar 2014 10:45:03 +0100 wenzelm tuned signature;
Tue, 18 Mar 2014 16:44:51 +0100 wenzelm clarified module arrangement;
Sat, 15 Mar 2014 11:59:18 +0100 wenzelm tuned signature;
Mon, 24 Feb 2014 14:58:40 +0100 wenzelm prefer standard Proof_Context.transfer, with theory stamp transfer (should now work thanks to purely functional theory, without Theory.copy etc.);
Tue, 30 Jul 2013 15:09:25 +0200 wenzelm type theory is purely value-oriented;
Sun, 30 Jun 2013 11:30:16 +0200 wenzelm just one alternative proof syntax, which also works for Proof_Syntax.pretty_proof/Proof_Syntax.read_proof roundtrip;
Sun, 16 Oct 2011 18:48:30 +0200 wenzelm added Term.dummy_pattern conveniences;
Tue, 19 Apr 2011 21:19:14 +0200 wenzelm eliminated obsolete Proof_Syntax.strip_sorts_consttypes;
Sun, 17 Apr 2011 19:54:04 +0200 wenzelm report Name_Space.declare/define, relatively to context;
Sat, 16 Apr 2011 15:47:52 +0200 wenzelm modernized structure Proof_Context;
Fri, 08 Apr 2011 16:34:14 +0200 wenzelm discontinued special treatment of structure Lexicon;
Tue, 05 Apr 2011 14:25:18 +0200 wenzelm discontinued special treatment of structure Ast: no pervasive content, no inclusion in structure Syntax;
Sun, 03 Apr 2011 21:59:33 +0200 wenzelm added Position.reports convenience;
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;
Sun, 12 Sep 2010 19:04:02 +0200 wenzelm eliminated aliases of Type.constraint;
Thu, 03 Jun 2010 23:56:05 +0200 wenzelm do not open Proofterm, which is very ould style;
Tue, 01 Jun 2010 11:30:57 +0200 berghofe merged
Tue, 01 Jun 2010 10:46:47 +0200 berghofe - Added extra flag to read_term and read_proof functions that allows to parse (proof)terms in which
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;
Wed, 28 Apr 2010 11:09:19 +0200 wenzelm modernized/simplified Sign.set_defsort;
Sat, 20 Mar 2010 17:33:11 +0100 wenzelm renamed varify/unvarify operations to varify_global/unvarify_global to emphasize that these only work in a global situation;
Sun, 21 Feb 2010 22:35:02 +0100 wenzelm slightly more abstract syntax mark/unmark operations;
Sat, 13 Feb 2010 23:16:06 +0100 wenzelm authentic proof syntax;
less more (0) -100 -60 tip