| Mon, 23 Jun 2008 15:51:37 +0200 |
wenzelm |
removed obsolete dest_concls;
|
file |
diff |
annotate
|
| Thu, 04 Oct 2001 14:49:38 +0200 |
wenzelm |
added dest_conj, dest_concls;
|
file |
diff |
annotate
|
| 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
|