src/HOL/Tools/Qelim/langford.ML
Wed, 31 Dec 2008 00:08:13 +0100 wenzelm moved old add_term_vars, add_term_frees etc. to structure OldTerm;
Tue, 31 Jul 2007 09:31:26 +0200 chaieb find_body goes under meta-quantifier ; tactic generalizes free variables;
Sun, 22 Jul 2007 17:53:54 +0200 chaieb Quantifier elimination for Dense linear orders after Langford
less more (0) tip