author | clasohm |
Thu, 19 Oct 1995 13:25:03 +0100 | |
changeset 1287 | 84f44b84d584 |
parent 1128 | 64b30e3cc6d4 |
child 1301 | 42782316d510 |
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