# HG changeset patch
# User nipkow
# Date 898618065 -7200
# Node ID 548f398d770b45dae7b818c4aab66a94b5d8002d
# Parent  c42429b3e2f2a5160b4c0f201343f7d47dc055a7
Consequences of the change from [ := ] to ( := ) in theory Update.

diff -r c42429b3e2f2 -r 548f398d770b src/HOL/UNITY/Mutex.thy
--- a/src/HOL/UNITY/Mutex.thy	Tue Jun 23 18:06:50 1998 +0200
+++ b/src/HOL/UNITY/Mutex.thy	Tue Jun 23 18:07:45 1998 +0200
@@ -26,24 +26,24 @@
 
 constdefs
   cmd0 :: "[pvar,pvar] => (state*state) set"
-    "cmd0 u m == {(s,s'). s' = s[u:=1][m:=1] & s m = 0}"
+    "cmd0 u m == {(s,s'). s' = s(u:=1,m:=1) & s m = 0}"
 
   cmd1u :: "(state*state) set"
-    "cmd1u == {(s,s'). s' = s[PP:= s VV][MM:=2] & s MM = 1}"
+    "cmd1u == {(s,s'). s' = s(PP:= s VV,MM:=2) & s MM = 1}"
 
   cmd1v :: "(state*state) set"
-    "cmd1v == {(s,s'). s' = s[PP:= 1 - s UU][NN:=2] & s NN = 1}"
+    "cmd1v == {(s,s'). s' = s(PP:= 1 - s UU,NN:=2) & s NN = 1}"
 
   (*Put pv=0 for u's program and pv=1 for v's program*)
   cmd2 :: "[nat,pvar] => (state*state) set"
-    "cmd2 pv m == {(s,s'). s' = s[m:=3] & s PP = pv & s m = 2}"
+    "cmd2 pv m == {(s,s'). s' = s(m:=3) & s PP = pv & s m = 2}"
 
   cmd3 :: "[pvar,pvar] => (state*state) set"
-    "cmd3 u m == {(s,s'). s' = s[u:=0][m:=4] & s m = 3}"
+    "cmd3 u m == {(s,s'). s' = s(u:=0,m:=4) & s m = 3}"
 
   (*Put pv=1 for u's program and pv=0 for v's program*)
   cmd4 :: "[nat,pvar] => (state*state) set"
-    "cmd4 pv m == {(s,s'). s' = s[PP:=pv][m:=0] & s m = 4}"
+    "cmd4 pv m == {(s,s'). s' = s(PP:=pv,m:=0) & s m = 4}"
 
   mutex :: "(state*state) set set"
     "mutex == {id,
diff -r c42429b3e2f2 -r 548f398d770b src/HOL/UNITY/Reach.ML
--- a/src/HOL/UNITY/Reach.ML	Tue Jun 23 18:06:50 1998 +0200
+++ b/src/HOL/UNITY/Reach.ML	Tue Jun 23 18:07:45 1998 +0200
@@ -134,19 +134,19 @@
 
 (*** Progress ***)
 
-Goalw [metric_def] "!!s. ~ s x ==> Suc (metric (s[x:=True])) = metric s";
-by (subgoal_tac "{v. ~ (s[x:=True]) v} = {v. ~ s v} - {x}" 1);
+Goalw [metric_def] "!!s. ~ s x ==> Suc (metric (s(x:=True))) = metric s";
+by (subgoal_tac "{v. ~ (s(x:=True)) v} = {v. ~ s v} - {x}" 1);
 by Auto_tac;
 by (asm_simp_tac (simpset() addsimps [card_Suc_Diff]) 1);
 qed "Suc_metric";
 
-Goal "!!s. ~ s x ==> metric (s[x:=True]) < metric s";
+Goal "!!s. ~ s x ==> metric (s(x:=True)) < metric s";
 by (etac (Suc_metric RS subst) 1);
 by (Blast_tac 1);
 qed "metric_less";
 AddSIs [metric_less];
 
-Goal "metric (s[y:=s x | s y]) <= metric s";
+Goal "metric (s(y:=s x | s y)) <= metric s";
 by (case_tac "s x --> s y" 1);
 by (auto_tac (claset() addIs [less_imp_le],
 	      simpset() addsimps [update_idem]));
diff -r c42429b3e2f2 -r 548f398d770b src/HOL/UNITY/Reach.thy
--- a/src/HOL/UNITY/Reach.thy	Tue Jun 23 18:06:50 1998 +0200
+++ b/src/HOL/UNITY/Reach.thy	Tue Jun 23 18:07:45 1998 +0200
@@ -21,7 +21,7 @@
 constdefs
 
   asgt  :: "[vertex,vertex] => (state*state) set"
-    "asgt u v == {(s,s'). s' = s[v:= s u | s v]}"
+    "asgt u v == {(s,s'). s' = s(v:= s u | s v)}"
 
   racts :: "(state*state) set set"
     "racts == insert id (UN (u,v): edges. {asgt u v})"