# HG changeset patch
# User paulson
# Date 902392623 -7200
# Node ID 212d203d6cd3778c19797d61b0467b1aad3e4fac
# Parent  ce3c25c8a694a862ba57cb6b1b00e8e63d003c08
New results from AC

diff -r ce3c25c8a694 -r 212d203d6cd3 src/ZF/Order.ML
--- a/src/ZF/Order.ML	Thu Aug 06 10:33:54 1998 +0200
+++ b/src/ZF/Order.ML	Thu Aug 06 10:37:03 1998 +0200
@@ -179,6 +179,22 @@
 qed "well_ord_0";
 
 
+(** The unit set is well-ordered by the empty relation (Grabczewski) **)
+
+Goalw [irrefl_def, trans_on_def, part_ord_def, linear_def, tot_ord_def]
+        "tot_ord({a},0)";
+by (Simp_tac 1);
+qed "tot_ord_unit";
+
+Goalw [wf_on_def, wf_def] "wf[{a}](0)";
+by (Fast_tac 1);
+qed "wf_on_unit";
+
+Goalw [well_ord_def] "well_ord({a},0)";
+by (simp_tac (simpset() addsimps [tot_ord_unit, wf_on_unit]) 1);
+qed "well_ord_unit";
+
+
 (** Order-preserving (monotone) maps **)
 
 Goalw [mono_map_def]