| changeset 753 | ec86863e87c8 |
| parent 435 | ca5356bd315a |
| child 1155 | 928a16e02f9f |
--- a/src/ZF/Rel.thy Mon Nov 28 19:48:30 1994 +0100 +++ b/src/ZF/Rel.thy Tue Nov 29 00:31:31 1994 +0100 @@ -12,7 +12,7 @@ sym,asym,antisym,trans :: "i=>o" trans_on :: "[i,i]=>o" ("trans[_]'(_')") -rules +defs refl_def "refl(A,r) == (ALL x: A. <x,x> : r)" irrefl_def "irrefl(A,r) == ALL x: A. <x,x> ~: r"