# 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,b>  == {{a,a}, {a,b}}"
   fst_def       "fst(p) == THE a. EX b. p=<a,b>"
   snd_def       "snd(p) == THE b. EX a. p=<a,b>"
-  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). {<x,y>}"
 
   (* Operations on relations *)
@@ -251,7 +251,7 @@
   domain_def    "domain(r) == {x. w:r, EX y. w=<x,y>}"
   range_def     "range(r) == domain(converse(r))"
   field_def     "field(r) == domain(r) Un range(r)"
-  function_def  "function(r) == ALL x y. <x,y>:r -->   
+  function_def  "function(r) == ALL x y. <x,y>:r -->
                                 (ALL y'. <x,y'>:r --> y=y')"
   image_def     "r `` A  == {y : range(r) . EX x:A. <x,y> : 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 *"))];