src/HOL/Tools/Qelim/langford.ML
2010-05-15 wenzelm 2010-05-15 less pervasive names from structure Thm;
2010-03-07 wenzelm 2010-03-07 modernized structure Object_Logic;
2010-02-27 wenzelm 2010-02-27 modernized structure Term_Ord;
2009-10-21 wenzelm 2009-10-21 standardized basic operations on type option;
2009-07-28 haftmann 2009-07-28 Set.UNIV and Set.empty are mere abbreviations for top and bot
2009-03-11 haftmann 2009-03-11 (restored previous version)
2009-03-11 haftmann 2009-03-11 HOLogic.mk_set, HOLogic.dest_set
2009-03-05 haftmann 2009-03-05 merged
2009-03-05 haftmann 2009-03-05 set operations Int, Un, INTER, UNION, Inter, Union, empty, UNIV are now proper qualified constants with authentic syntax
2009-02-27 wenzelm 2009-02-27 eliminated private clones of List.partition;
2008-12-31 wenzelm 2008-12-31 moved term order operations to structure TermOrd (cf. Pure/term_ord.ML); tuned signature of structure Term;
2008-12-31 wenzelm 2008-12-31 moved old add_term_vars, add_term_frees etc. to structure OldTerm;
2007-07-31 chaieb 2007-07-31 find_body goes under meta-quantifier ; tactic generalizes free variables;
2007-07-22 chaieb 2007-07-22 Quantifier elimination for Dense linear orders after Langford