# HG changeset patch
# User nipkow
# Date 898618010 -7200
# Node ID c42429b3e2f2a5160b4c0f201343f7d47dc055a7
# Parent  3ea049f7979dc7ba220e95c7cc75e0a5b73d7f03
Replaced [ := ] syntax by ( := ).
Also allows ( := , := , ...) now.

diff -r 3ea049f7979d -r c42429b3e2f2 src/HOL/Update.ML
--- a/src/HOL/Update.ML	Mon Jun 22 17:26:46 1998 +0200
+++ b/src/HOL/Update.ML	Tue Jun 23 18:06:50 1998 +0200
@@ -8,19 +8,19 @@
 
 open Update;
 
-Goalw [update_def] "(f[x:=y] = f) = (f x = y)";
+Goalw [update_def] "(f(x:=y) = f) = (f x = y)";
 by Safe_tac;
 by (etac subst 1);
 by (rtac ext 2);
 by Auto_tac;
 qed "update_idem_iff";
 
-(* f x = y ==> f[x:=y] = f *)
+(* f x = y ==> f(x:=y) = f *)
 bind_thm("update_idem", update_idem_iff RS iffD2);
 
 AddIffs [refl RS update_idem];
 
-Goal "(f[x:=y])z = (if x=z then y else f z)";
+Goal "(f(x:=y))z = (if x=z then y else f z)";
 by (simp_tac (simpset() addsimps [update_def]) 1);
 qed "update_apply";
 Addsimps [update_apply];
diff -r 3ea049f7979d -r c42429b3e2f2 src/HOL/Update.thy
--- a/src/HOL/Update.thy	Mon Jun 22 17:26:46 1998 +0200
+++ b/src/HOL/Update.thy	Tue Jun 23 18:06:50 1998 +0200
@@ -10,9 +10,24 @@
 
 consts
   update  :: "('a => 'b) => 'a => 'b => ('a => 'b)"
-           ("_/[_/:=/_]" [900,0,0] 900)
+
+nonterminals
+  updbinds  updbind
+
+syntax
+
+  (* Let expressions *)
+
+  "_updbind"       :: ['a, 'a] => updbind             ("(2_ :=/ _)")
+  ""               :: updbind => updbinds             ("_")
+  "_updbinds"      :: [updbind, updbinds] => updbinds ("_,/ _")
+  "_Update"        :: ['a, updbinds] => 'a            ("_/'((_)')" [900,0] 900)
+
+translations
+  "_Update f (_updbinds b bs)"  == "_Update (_Update f b) bs"
+  "f(x:=y)"                     == "update f x y"
 
 defs
-  update_def "f[a:=b] == %x. if x=a then b else f x"
+  update_def "f(a:=b) == %x. if x=a then b else f x"
 
 end