src/HOL/Decision_Procs/ferrack_tac.ML
2012-03-25 ago merged fork with new numeral representation (see NEWS)
2011-11-27 ago more antiquotations;
2011-08-10 ago old term operations are legacy;
2011-04-16 ago modernized structure Proof_Context;
2011-03-24 ago added Term.is_open and Term.is_dependent convenience, to cover common situations of loose bounds;
2010-08-19 ago tuned quotes
2010-08-19 ago use antiquotations for remaining unqualified constants in HOL
2010-05-15 ago less pervasive names from structure Thm;
2010-05-12 ago modernized specifications; tuned reification
2010-05-05 ago farewell to old-style mem infixes -- type inference in situations with mem_int and mem_string should provide enough information to resolve the type of (op =)
2010-03-07 ago modernized structure Object_Logic;
2010-02-19 ago local Simplifier.context;
2010-02-19 ago renamed Simplifier.theory_context to Simplifier.global_context to emphasize that this is not the real thing;
2009-10-19 ago always qualify NJ's old List.foldl/foldr in Isabelle/ML;
2009-10-17 ago eliminated hard tabulators, guessing at each author's individual tab-width;
2009-09-29 ago explicit indication of Unsynchronized.ref;
2009-06-24 ago corrected and unified thm names
2009-05-30 ago proper signature constraint;
2009-03-13 ago unified type Proof.method and pervasive METHOD combinators;
2009-03-11 ago Updated paths in Decision_Procs comments and NEWS
2009-03-04 ago Merge.
2009-03-04 ago Merge.
2009-03-03 ago removed and renamed redundant lemmas
2009-02-21 ago removed redundant thms
2009-02-17 ago Cleaned up IntDiv and removed subsumed lemmas.
2009-02-06 ago session Reflecion renamed to Decision_Procs, moved Dense_Linear_Order there