author | paulson |
Thu, 21 Nov 1996 15:19:09 +0100 | |
changeset 2214 | f869dc885841 |
parent 1478 | 2b8c2a7547ab |
child 2469 | b50b8c0eec01 |
permissions | -rw-r--r-- |
(* Title: ZF/trancl.thy ID: $Id$ Author: Lawrence C Paulson, Cambridge University Computer Laboratory Copyright 1992 University of Cambridge Transitive closure of a relation *) Trancl = Fixedpt + Perm + "mono" + Rel + consts rtrancl :: i=>i ("(_^*)" [100] 100) (*refl/transitive closure*) trancl :: i=>i ("(_^+)" [100] 100) (*transitive closure*) defs rtrancl_def "r^* == lfp(field(r)*field(r), %s. id(field(r)) Un (r O s))" trancl_def "r^+ == r O r^*" end