--- a/src/HOL/Hyperreal/Filter.ML Fri Aug 30 16:42:45 2002 +0200
+++ b/src/HOL/Hyperreal/Filter.ML Sat Aug 31 14:03:49 2002 +0200
@@ -5,6 +5,12 @@
Description : Filters and Ultrafilter
*)
+(*ML bindings for Library/Zorn theorems*)
+val chain_def = thm "chain_def";
+val chainD = thm "chainD";
+val chainD2 = thm "chainD2";
+val Zorn_Lemma2 = thm "Zorn_Lemma2";
+
(*------------------------------------------------------------------
Properties of Filters and Freefilters -
rules for intro, destruction etc.