author | wenzelm |
Wed, 15 Oct 1997 15:12:59 +0200 | |
changeset 3872 | a5839ecee7b8 |
parent 1478 | 2b8c2a7547ab |
child 11319 | 8b84ee2cc79c |
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