# HG changeset patch # User paulson # Date 1011086638 -3600 # Node ID a0c0a1e3a53add355dc14e348762bd1f67418e9a # Parent b0c39f9837af6ebfe6cdf4ea3e0df27ea397c796 split can now be unfolded even with one argument diff -r b0c39f9837af -r a0c0a1e3a53a src/ZF/ZF.thy --- a/src/ZF/ZF.thy Tue Jan 15 00:13:20 2002 +0100 +++ b/src/ZF/ZF.thy Tue Jan 15 10:23:58 2002 +0100 @@ -6,7 +6,7 @@ Zermelo-Fraenkel Set Theory *) -ZF = FOL + Let + +ZF = FOL + Let + global @@ -198,7 +198,7 @@ foundation "A=0 | (EX x:A. ALL y:x. y~:A)" (*Schema axiom since predicate P is a higher-order variable*) - replacement "(ALL x:A. ALL y z. P(x,y) & P(x,z) --> y=z) ==> + replacement "(ALL x:A. ALL y z. P(x,y) & P(x,z) --> y=z) ==> b : PrimReplace(A,P) <-> (EX x:A. P(x,b))" defs @@ -240,7 +240,7 @@ Pair_def " == {{a,a}, {a,b}}" fst_def "fst(p) == THE a. EX b. p=" snd_def "snd(p) == THE b. EX a. p=" - split_def "split(c,p) == c(fst(p), snd(p))" + split_def "split(c) == %p. c(fst(p), snd(p))" Sigma_def "Sigma(A,B) == UN x:A. UN y:B(x). {}" (* Operations on relations *) @@ -251,7 +251,7 @@ domain_def "domain(r) == {x. w:r, EX y. w=}" range_def "range(r) == domain(converse(r))" field_def "field(r) == domain(r) Un range(r)" - function_def "function(r) == ALL x y. :r --> + function_def "function(r) == ALL x y. :r --> (ALL y'. :r --> y=y')" image_def "r `` A == {y : range(r) . EX x:A. : r}" vimage_def "r -`` A == converse(r)``A" @@ -272,7 +272,7 @@ (* Pattern-matching and 'Dependent' type operators *) -val print_translation = +val print_translation = [(*("split", split_tr'),*) ("Pi", dependent_tr' ("@PROD", "op ->")), ("Sigma", dependent_tr' ("@SUM", "op *"))];