src/Pure/Proof/proofchecker.ML
2008-10-23 wenzelm 2008-10-23 renamed Thm.get_axiom_i to Thm.axiom;
2008-05-18 wenzelm 2008-05-18 moved global pretty/string_of functions from Sign to Syntax;
2007-05-10 wenzelm 2007-05-10 moved conversions to structure Conv; get_axiom_i;
2006-12-05 wenzelm 2006-12-05 thm/prf: separate official name vs. additional tags;
2006-07-19 wenzelm 2006-07-19 thm_of_proof: improved generation of variables;
2006-07-18 wenzelm 2006-07-18 thm_of_proof: tuned Name operations;
2006-07-11 wenzelm 2006-07-11 replaced Term.variant(list) by Name.variant(_list);
2005-11-09 wenzelm 2005-11-09 Thm.varifyT': natural argument order;
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-07-15 wenzelm 2005-07-15 tuned;
2005-06-29 wenzelm 2005-06-29 Drule.implies_intr_hyps;
2005-06-09 wenzelm 2005-06-09 PureThy.all_thms_of;
2005-04-21 berghofe 2005-04-21 Adapted to new interface of instantiation and unification / matching functions.
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-23 skalberg 2004-06-23 Moved conversion rules from MetaSimplifier to Drule. refl_implies removed from Drule, instead imp_cong' exported from there.
2004-06-21 kleing 2004-06-21 Merged in license change from Isabelle2004
2002-11-27 berghofe 2002-11-27 - tuned beta_eta_convert - returned theorem is now in beta-eta normal form
2002-10-21 berghofe 2002-10-21 Fixed problem with theorems containing TFrees.
2001-11-19 berghofe 2001-11-19 Improved error message.
2001-09-28 berghofe 2001-09-28 Exchanged % and %%.
2001-08-31 wenzelm 2001-08-31 tuned headers;
2001-08-31 berghofe 2001-08-31 Initial revision of tools for proof terms.