src/Pure/Proof/proof_syntax.ML
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.
2002-02-20 berghofe 2002-02-20 Moved change_type to proofterm.ML
2001-10-19 wenzelm 2001-10-19 latex output: bold lambda;
2001-09-30 berghofe 2001-09-30 Tuned indentation of abstractions.
2001-09-28 berghofe 2001-09-28 - Tuned syntax - proof_of_term: fixed problems with dummy patterns and typing information
2001-08-31 wenzelm 2001-08-31 tuned headers;
2001-08-31 berghofe 2001-08-31 Initial revision of tools for proof terms.