diff -r 7330e4eefbd7 -r 426d5781bb25 src/HOL/UNITY/Comp/Counterc.thy
--- a/src/HOL/UNITY/Comp/Counterc.thy	Wed May 12 15:25:58 2010 +0200
+++ b/src/HOL/UNITY/Comp/Counterc.thy	Wed May 12 16:44:49 2010 +0200
@@ -33,12 +33,12 @@
 types command = "(state*state)set"
 
 definition a :: "nat=>command" where
- "a i == {(s, s'). (c s') i = (c s) i + 1 & (C s') = (C s) + 1}"
+ "a i = {(s, s'). (c s') i = (c s) i + 1 & (C s') = (C s) + 1}"
  
 definition Component :: "nat => state program" where
-  "Component i == mk_total_program({s. C s = 0 & (c s) i = 0},
-                                   {a i},
-                                   \<Union>G \<in> preserves (%s. (c s) i). Acts G)"
+  "Component i = mk_total_program({s. C s = 0 & (c s) i = 0},
+                                  {a i},
+                                  \<Union>G \<in> preserves (%s. (c s) i). Acts G)"
 
 
 declare Component_def [THEN def_prg_Init, simp]