src/Pure/Proof/proof_syntax.ML
2016-04-12 wenzelm 2016-04-12 Type_Infer.object_logic controls improvement of type inference result;
2016-04-09 wenzelm 2016-04-09 clarified context; avoid Unsynchronized.ref;
2016-03-30 wenzelm 2016-03-30 clarified simple mixfix;
2016-03-29 wenzelm 2016-03-29 more position information for type mixfix;
2015-12-29 wenzelm 2015-12-29 former "xsymbols" syntax is used by default, and ASCII replacement syntax with print mode "ASCII"; uniform syntax for Pure.imp; removed obsolete "HTML" syntax;
2015-07-28 wenzelm 2015-07-28 clarified context;
2015-03-06 wenzelm 2015-03-06 Thm.cterm_of and Thm.ctyp_of operate on local context;
2015-03-04 wenzelm 2015-03-04 tuned signature -- prefer qualified names;
2014-04-06 wenzelm 2014-04-06 more source positions;
2014-03-21 wenzelm 2014-03-21 more qualified names;
2014-03-21 wenzelm 2014-03-21 more qualified names;
2014-03-21 wenzelm 2014-03-21 tuned signature;
2014-03-21 wenzelm 2014-03-21 tuned signature;
2014-03-18 wenzelm 2014-03-18 clarified module arrangement; more antiquotations;
2014-03-15 wenzelm 2014-03-15 tuned signature; eliminated clones;
2014-02-24 wenzelm 2014-02-24 prefer standard Proof_Context.transfer, with theory stamp transfer (should now work thanks to purely functional theory, without Theory.copy etc.);
2013-07-30 wenzelm 2013-07-30 type theory is purely value-oriented;
2013-06-30 wenzelm 2013-06-30 just one alternative proof syntax, which also works for Proof_Syntax.pretty_proof/Proof_Syntax.read_proof roundtrip;
2011-10-16 wenzelm 2011-10-16 added Term.dummy_pattern conveniences;
2011-04-19 wenzelm 2011-04-19 eliminated obsolete Proof_Syntax.strip_sorts_consttypes;
2011-04-17 wenzelm 2011-04-17 report Name_Space.declare/define, relatively to context; added "global" variants of context-dependent declarations;
2011-04-16 wenzelm 2011-04-16 modernized structure Proof_Context;
2011-04-08 wenzelm 2011-04-08 discontinued special treatment of structure Lexicon;
2011-04-05 wenzelm 2011-04-05 discontinued special treatment of structure Ast: no pervasive content, no inclusion in structure Syntax;
2011-04-03 wenzelm 2011-04-03 added Position.reports convenience; modernized Syntax.trrule constructors; modernized Sign.add_trrules/del_trrules: internal arguments; modernized Isar_Cmd.translations/no_translations: external arguments; explicit syntax categories class_name/type_name, with reports via type_context; eliminated former class_name/type_name ast translations; tuned signatures;
2010-09-20 wenzelm 2010-09-20 renamed structure PureThy to Pure_Thy and moved most content to Global_Theory, to emphasize that this is global-only;
2010-09-12 wenzelm 2010-09-12 eliminated aliases of Type.constraint;
2010-06-03 wenzelm 2010-06-03 do not open Proofterm, which is very ould style;
2010-06-01 berghofe 2010-06-01 merged
2010-06-01 berghofe 2010-06-01 - Added extra flag to read_term and read_proof functions that allows to parse (proof)terms in which all type variables have the top sort - Adapted proof_of_term to handle proofs with explicit class membership proofs
2010-05-27 wenzelm 2010-05-27 renamed structure TypeInfer to Type_Infer, keeping the old name as legacy alias for some time;
2010-05-03 wenzelm 2010-05-03 renamed ProofContext.init to ProofContext.init_global to emphasize that this is not the real thing;
2010-04-28 wenzelm 2010-04-28 modernized/simplified Sign.set_defsort;
2010-03-20 wenzelm 2010-03-20 renamed varify/unvarify operations to varify_global/unvarify_global to emphasize that these only work in a global situation;
2010-02-21 wenzelm 2010-02-21 slightly more abstract syntax mark/unmark operations;
2010-02-13 wenzelm 2010-02-13 authentic proof syntax;
2009-11-02 wenzelm 2009-11-02 modernized structure Proof_Syntax;
2009-07-06 wenzelm 2009-07-06 renamed inclass/Inclass to of_class/OfClass, in accordance to of_sort;
2009-07-02 wenzelm 2009-07-02 added pro-forma proof constructor Inclass;
2009-03-11 wenzelm 2009-03-11 explicit Binding.qualified_name -- prevents implicitly qualified bstring;
2009-03-08 wenzelm 2009-03-08 moved basic algebra of long names from structure NameSpace to Long_Name;
2009-03-07 wenzelm 2009-03-07 more uniform handling of binding in targets and derived elements;
2009-01-27 wenzelm 2009-01-27 proof_body: turned lazy into future -- ensures that body is fulfilled eventually, without explicit force;
2009-01-21 wenzelm 2009-01-21 removed Ids;
2008-11-16 wenzelm 2008-11-16 clarified Thm.proof_body_of vs. Thm.proof_of;
2008-11-15 wenzelm 2008-11-15 proof_of_term: removed obsolete disambiguisation table; adapted PThm; Thm.proof_of returns proof_body;
2008-09-26 wenzelm 2008-09-26 eliminated polymorphic equality;
2008-06-18 wenzelm 2008-06-18 moved ProofContext.pretty_proof to ProofSyntax.pretty_proof; read_term: imitate old behaviour (allow_dummies, mode_schematic);
2008-05-18 wenzelm 2008-05-18 moved global pretty/string_of functions from Sign to Syntax;
2008-04-12 wenzelm 2008-04-12 rep_cterm/rep_thm: no longer dereference theory_ref;
2007-10-30 berghofe 2007-10-30 Added well-formedness check to Abst case in function prf_of.
2007-10-04 wenzelm 2007-10-04 replaced literal 'a by Name.aT;
2007-04-26 wenzelm 2007-04-26 renamed some old names Theory.xxx to Sign.xxx;
2007-04-14 wenzelm 2007-04-14 cleaned/simplified Sign.read_typ, Thm.read_cterm etc.;
2006-12-15 wenzelm 2006-12-15 avoid conflict with Alice keywords: renamed pack -> implode, unpack -> explode, any -> many, avoided assert;
2006-12-05 wenzelm 2006-12-05 thm/prf: separate official name vs. additional tags;
2006-10-20 haftmann 2006-10-20 Symtab.foldl replaced by Symtab.fold
2006-09-15 wenzelm 2006-09-15 renamed Term.map_term_types to Term.map_types (cf. Term.fold_types);
2006-05-11 wenzelm 2006-05-11 tuned;
2006-04-26 wenzelm 2006-04-26 tuned;