src/Pure/more_thm.ML
2008-10-23 wenzelm 2008-10-23 renamed Thm.get_axiom_i to Thm.axiom;
2008-10-16 wenzelm 2008-10-16 added check_shyps, which reject pending sort hypotheses;
2008-09-03 wenzelm 2008-09-03 simplified add_axiom: no hyps;
2008-08-27 wenzelm 2008-08-27 type Properties.T;
2008-08-14 wenzelm 2008-08-14 moved basic thm operations from structure PureThy to Thm; added position operations; tuned;
2008-06-18 wenzelm 2008-06-18 removed obsolete read_def_cterms/read_cterm;
2008-04-15 wenzelm 2008-04-15 Theory.eq_thy;
2008-04-15 wenzelm 2008-04-15 Thm.forall_elim_var(s);
2008-04-12 wenzelm 2008-04-12 replaced Drule.close_derivation/Goal.close_result by Thm.close_derivation (removed obsolete compression);
2007-12-03 haftmann 2007-12-03 interface for unchecked definitions
2007-10-11 wenzelm 2007-10-11 added elim_implies (more convenient argument order); added unvarify (from drule.ML); added specification primitives: add_axiom, add_def;
2007-10-10 wenzelm 2007-10-10 tuned;
2007-09-30 wenzelm 2007-09-30 Markup.internalK;
2007-07-29 wenzelm 2007-07-29 moved Drule.add/del/merge_rules to Thm.add/del/merge_thms; moved Drule.is_dummy_thm to Thm.is_dummy;
2007-07-05 wenzelm 2007-07-05 added is_reflexive;
2007-06-25 wenzelm 2007-06-25 added reasonably efficient add_cterm_frees;
2007-05-31 wenzelm 2007-05-31 made aconvc pervasive;
2007-05-31 wenzelm 2007-05-31 moved aconvc to more_thm.ML;
2007-05-10 wenzelm 2007-05-10 added destructors from drule.ML; added mk_binop;
2007-04-15 wenzelm 2007-04-15 moved Drule.plain_prop_of, Drule.fold_terms to more_thm.ML;
2007-04-14 wenzelm 2007-04-14 added read_def_cterms, read_cterm (from thm.ML);
2007-02-28 wenzelm 2007-02-28 tuned;
2007-02-26 wenzelm 2007-02-26 Further operations on type thm, outside the inference kernel.