1.1 --- a/src/HOL/UNITY/Comp/Progress.thy	Tue Feb 21 17:08:32 2012 +0100
     1.2 +++ b/src/HOL/UNITY/Comp/Progress.thy	Tue Feb 21 17:09:17 2012 +0100
     1.3 @@ -13,10 +13,10 @@
     1.4  text{*Thesis Section 4.4.2*}
     1.5  
     1.6  definition FF :: "int program" where
     1.7 -    "FF == mk_total_program (UNIV, {range (\<lambda>x. (x, x+1))}, UNIV)"
     1.8 +    "FF = mk_total_program (UNIV, {range (\<lambda>x. (x, x+1))}, UNIV)"
     1.9  
    1.10  definition GG :: "int program" where
    1.11 -    "GG == mk_total_program (UNIV, {range (\<lambda>x. (x, 2*x))}, UNIV)"
    1.12 +    "GG = mk_total_program (UNIV, {range (\<lambda>x. (x, 2*x))}, UNIV)"
    1.13  
    1.14  subsubsection {*Calculating @{term "wens_set FF (atLeast k)"}*}
    1.15