src/ZF/Trancl.thy
changeset 2469 b50b8c0eec01
parent 1478 2b8c2a7547ab
child 13220 62c899c77151
equal deleted inserted replaced
2468:428efffe8599 2469:b50b8c0eec01
     4     Copyright   1992  University of Cambridge
     4     Copyright   1992  University of Cambridge
     5 
     5 
     6 Transitive closure of a relation
     6 Transitive closure of a relation
     7 *)
     7 *)
     8 
     8 
     9 Trancl = Fixedpt + Perm + "mono" + Rel + 
     9 Trancl = Fixedpt + Perm + mono + Rel + 
    10 consts
    10 consts
    11     rtrancl :: i=>i  ("(_^*)" [100] 100)  (*refl/transitive closure*)
    11     rtrancl :: i=>i  ("(_^*)" [100] 100)  (*refl/transitive closure*)
    12     trancl  :: i=>i  ("(_^+)" [100] 100)  (*transitive closure*)
    12     trancl  :: i=>i  ("(_^+)" [100] 100)  (*transitive closure*)
    13 
    13 
    14 defs
    14 defs