Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/ZF/Order.thy
changeset 578 efc648d29dd0
parent 435 ca5356bd315a
child 786 2a871417e7fc 
--- a/src/ZF/Order.thy	Thu Aug 25 10:41:17 1994 +0200
+++ b/src/ZF/Order.thy	Thu Aug 25 12:09:21 1994 +0200
@@ -14,7 +14,7 @@
   ord_iso         :: "[i,i,i,i]=>i"	(*Order isomorphisms*)
   pred            :: "[i,i,i]=>i"	(*Set of predecessors*)
 
-rules
+defs
   part_ord_def "part_ord(A,r) == irrefl(A,r) & trans[A](r)"
 
   linear_def   "linear(A,r) == (ALL x:A. ALL y:A. <x,y>:r | x=y | <y,x>:r)"
isabelle