src/Provers/quantifier1.ML
2006-07-08 wenzelm 2006-07-08 Goal.prove: context;
2005-10-21 wenzelm 2005-10-21 Goal.prove;
2005-08-02 wenzelm 2005-08-02 simprocs: Simplifier.inherit_bounds;
2005-02-13 skalberg 2005-02-13 Deleted Library.option type.
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.