diff -r dc281bd5ca0a -r a3f592e3f4bd src/ZF/UNITY/GenPrefix.thy
--- a/src/ZF/UNITY/GenPrefix.thy	Fri May 30 11:44:29 2003 +0200
+++ b/src/ZF/UNITY/GenPrefix.thy	Mon Jun 02 11:17:52 2003 +0200
@@ -13,6 +13,10 @@
 
 GenPrefix = Main + 
 
+constdefs (*really belongs in ZF/Trancl*)
+  part_order :: [i, i] => o
+  "part_order(A, r) == refl(A,r) & trans[A](r) & antisym(r)"
+
 consts
   gen_prefix :: "[i, i] => i"