author | oheimb |
Fri, 12 Jul 1996 20:46:32 +0200 (1996-07-12) | |
changeset 1858 | 513316fd1087 |
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