src/Provers/quantifier1.ML
2004-07-08 wenzelm 2004-07-08 adapted type of simprocs;
2002-08-08 wenzelm 2002-08-08 use Tactic.prove instead of prove_goalw_cterm in internal proofs!
2001-12-17 nipkow 2001-12-17 now permutations of quantifiers are allowed as well.
2001-03-29 nipkow 2001-03-29 generalization of 1 point rules for ALL
2001-03-23 nipkow 2001-03-23 added simproc for bounded quantifiers
1999-10-27 nipkow 1999-10-27 Fixed a bug in the EX simproc.
1997-11-28 nipkow 1997-11-28 Quantifier elimination procs.