changeset 14854 | 61bdf2ae4dc5 |
parent 13823 | d49ffd9f9662 |
child 16417 | 9bc16273c2d4 |
--- a/src/ZF/QPair.thy Tue Jun 01 11:25:26 2004 +0200 +++ b/src/ZF/QPair.thy Tue Jun 01 12:33:50 2004 +0200 @@ -31,7 +31,7 @@ qsnd :: "i => i" "qsnd(p) == THE b. EX a. p=<a;b>" - qsplit :: "[[i, i] => 'a, i] => 'a::logic" (*for pattern-matching*) + qsplit :: "[[i, i] => 'a, i] => 'a::{}" (*for pattern-matching*) "qsplit(c,p) == c(qfst(p), qsnd(p))" qconverse :: "i => i"