| changeset 14055 | a3f592e3f4bd |
| parent 14046 | 6616e6c53d48 |
| child 15634 | bca33c49b083 |
--- 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"