src/HOL/Tools/Qelim/langford.ML
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