src/HOL/Tools/Qelim/ferrante_rackoff.ML
2010-03-07 wenzelm 2010-03-07 modernized structure Object_Logic;
2009-07-28 haftmann 2009-07-28 Set.UNIV and Set.empty are mere abbreviations for top and bot
2009-07-23 wenzelm 2009-07-23 renamed simpset_of to global_simpset_of, and local_simpset_of to simpset_of -- same for claset and clasimpset;
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
2007-09-15 haftmann 2007-09-15 fixed title
2007-07-04 wenzelm 2007-07-04 export dlo_conv; removed redundant auxiliary operations; tuned exceptions -- avoid error here; simplified tactic wrapper (CSUBGOAL, CONVERSION); merge_ss: recover simpset context; tuned;
2007-07-02 chaieb 2007-07-02 Generic QE need no Context anymore
2007-06-25 wenzelm 2007-06-25 Thm.add_cterm_frees;
2007-06-21 wenzelm 2007-06-21 moved quantifier elimination tools to Tools/Qelim/;