src/Pure/Proof/proof_syntax.ML
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;
2006-04-10 wenzelm 2006-04-10 Term.itselfT;
2006-03-21 wenzelm 2006-03-21 avoid polymorphic equality;
2006-02-06 wenzelm 2006-02-06 tuned;
2005-09-15 wenzelm 2005-09-15 TableFun/Symtab: curried lookup and update;
2005-09-01 wenzelm 2005-09-01 curried_lookup/update; tuned;
2005-08-16 wenzelm 2005-08-16 export proof_syntax, proof_of;
2005-08-03 berghofe 2005-08-03 Adapted to new interface og thms_of_proof / axms_of_proof.
2005-07-15 wenzelm 2005-07-15 tuned assoc;
2005-06-17 wenzelm 2005-06-17 accomodate identification of type Sign.sg and theory;
2005-06-09 wenzelm 2005-06-09 Theory.all_axioms_of, PureThy.all_thms_of;
2005-06-02 wenzelm 2005-06-02 tuned;
2005-06-02 wenzelm 2005-06-02 swap declaration of thm/axm names to accomodate change in name space treatment;
2005-03-04 skalberg 2005-03-04 Removed practically all references to Library.foldr.
2005-03-03 skalberg 2005-03-03 Move towards standard functions.
2005-02-13 skalberg 2005-02-13 Deleted Library.option type.
2004-06-21 kleing 2004-06-21 Merged in license change from Isabelle2004
2004-06-01 wenzelm 2004-06-01 removed obsolete sort 'logic';
2002-08-27 wenzelm 2002-08-27 Thm.proof_of;
2002-05-31 berghofe 2002-05-31 Added constants for Hyp, Oracle and MinProof.