Thu, 08 Jul 2004 19:34:56 +0200 | wenzelm | adapted type of simprocs; | file | diff | annotate |
Thu, 08 Aug 2002 23:46:09 +0200 | wenzelm | use Tactic.prove instead of prove_goalw_cterm in internal proofs! | file | diff | annotate |
Mon, 17 Dec 2001 14:21:59 +0100 | nipkow | now permutations of quantifiers are allowed as well. | file | diff | annotate |
Thu, 29 Mar 2001 13:59:54 +0200 | nipkow | generalization of 1 point rules for ALL | file | diff | annotate |
Fri, 23 Mar 2001 10:12:12 +0100 | nipkow | added simproc for bounded quantifiers | file | diff | annotate |
Wed, 27 Oct 1999 17:17:28 +0200 | nipkow | Fixed a bug in the EX simproc. | file | diff | annotate |
Fri, 28 Nov 1997 07:35:47 +0100 | nipkow | Quantifier elimination procs. | file | diff | annotate |