| changeset 27704 | 5b1585b48952 |
| parent 27696 | 15b65db66751 |
| child 27713 | 95b36bfe7fc4 |
--- a/NEWS Tue Jul 29 17:50:12 2008 +0200 +++ b/NEWS Tue Jul 29 17:50:48 2008 +0200 @@ -147,6 +147,11 @@ Complex_Main.thy should now use new entry point Hypercomplex.thy. +*** ZF *** + +* Proof of Zorn's Lemma for partial orders. + + *** ML *** * Rules and tactics that read instantiations (read_instantiate,