author | regensbu |
Fri, 06 Oct 1995 16:17:08 +0100 | |
changeset 1273 | 6960ec882bca |
parent 1128 | 64b30e3cc6d4 |
child 1287 | 84f44b84d584 |
permissions | -rw-r--r-- |
(* Title: HOL/trancl.thy ID: $Id$ Author: Lawrence C Paulson, Cambridge University Computer Laboratory Copyright 1992 University of Cambridge Relfexive and Transitive closure of a relation rtrancl is refl&transitive closure; trancl is transitive closure *) Trancl = Lfp + Relation + consts rtrancl :: "('a * 'a)set => ('a * 'a)set" ("(_^*)" [100] 100) trancl :: "('a * 'a)set => ('a * 'a)set" ("(_^+)" [100] 100) defs rtrancl_def "r^* == lfp(%s. id Un (r O s))" trancl_def "r^+ == r O rtrancl(r)" end