| Fri, 03 Nov 2000 21:31:53 +0100 | wenzelm | removed atomic_Trueprop (now in Pure/Isar/auto_bind.ML); | file | diff | annotate |
| Tue, 05 Sep 2000 18:45:51 +0200 | wenzelm | added not; | file | diff | annotate |
| Mon, 07 Aug 2000 10:26:02 +0200 | paulson | new abstract syntax operations, used in ZF | file | diff | annotate |
| Sun, 30 Jul 2000 13:02:14 +0200 | wenzelm | added atomic_Trueprop; | file | diff | annotate |
| Mon, 04 Oct 1999 21:35:26 +0200 | wenzelm | added mk_conj, mk_disj, mk_imp; | file | diff | annotate |
| Tue, 19 Jan 1999 11:16:39 +0100 | paulson | tidied; added dest_eq | file | diff | annotate |
| Tue, 23 Dec 1997 11:39:03 +0100 | paulson | Better equality handling in Blast_tac, usingd a new variant of hyp_subst_tac | file | diff | annotate |
| Wed, 03 Dec 1997 10:48:16 +0100 | paulson | Instantiated the one-point-rule quantifier simpprocs for FOL | file | diff | annotate |