author | clasohm |
Sat, 09 Dec 1995 13:36:11 +0100 | |
changeset 1401 | 0c439768f45c |
parent 1155 | 928a16e02f9f |
child 1478 | 2b8c2a7547ab |
permissions | -rw-r--r-- |
(* Title: Confluence.thy ID: $Id$ Author: Ole Rasmussen Copyright 1995 University of Cambridge Logic Image: ZF *) Confluence = Reduction+ consts confluence :: i=>o strip :: o defs confluence_def "confluence(R) == ALL x y. <x,y>:R --> (ALL z.<x,z>:R --> (EX u.<y,u>:R & <z,u>:R))" strip_def "strip == ALL x y. (x ===> y) --> (ALL z.(x =1=> z) --> (EX u.(y =1=> u) & (z===>u)))" end