src/ZF/func.thy
changeset 41229 d797baa3d57c
parent 32960 69916a850301
child 46820 c656222c4dc1
--- a/src/ZF/func.thy	Fri Dec 17 17:08:56 2010 +0100
+++ b/src/ZF/func.thy	Fri Dec 17 17:43:54 2010 +0100
@@ -445,8 +445,7 @@
   update  :: "[i,i,i] => i"  where
    "update(f,a,b) == lam x: cons(a, domain(f)). if(x=a, b, f`x)"
 
-nonterminals
-  updbinds  updbind
+nonterminal updbinds and updbind
 
 syntax