src/Provers/quantifier1.ML
2014-10-30 wenzelm 2014-10-30 eliminated aliases;
2014-01-12 wenzelm 2014-01-12 tuned signature; clarified context;
2013-04-18 wenzelm 2013-04-18 simplifier uses proper Proof.context instead of historic type simpset;
2011-04-22 wenzelm 2011-04-22 simplified Data signature;
2011-04-22 wenzelm 2011-04-22 misc tuning and simplification;
2011-04-22 wenzelm 2011-04-22 misc tuning;
2011-04-22 wenzelm 2011-04-22 do not open ML structures;
2011-04-22 wenzelm 2011-04-22 proper context for Quantifier1 simprocs (avoid bad ProofContext.init_global from abc655166d61); tuned signature;
2011-04-16 wenzelm 2011-04-16 modernized structure Proof_Context;
2010-08-17 blanchet 2010-08-17 merged
2010-08-16 blanchet 2010-08-16 typos in comment
2010-08-17 nipkow 2010-08-17 now works for schematic terms as well, thanks to Alex for the `how-to'
2010-05-03 wenzelm 2010-05-03 renamed ProofContext.init to ProofContext.init_global to emphasize that this is not the real thing;
2010-03-13 wenzelm 2010-03-13 removed old CVS Ids; tuned headers;
2009-05-18 nipkow 2009-05-18 fine-tuned elimination of comprehensions involving x=t.
2009-05-16 nipkow 2009-05-16 "{x. P x & x=t & Q x}" is now rewritten to "if P t & Q t then {t} else {}" by the new simproc defColl_regroup. More precisely, the simproc pulls an equation x=t (or t=x) out of a nest of conjunctions to the front where the simp rule singleton_conj_conv(2) converts to "if".
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.