1.1 --- a/src/HOL/Partial_Function.thy	Fri Oct 28 16:49:15 2011 +0200
     1.2 +++ b/src/HOL/Partial_Function.thy	Sat Oct 29 12:55:34 2011 +0200
     1.3 @@ -127,7 +127,7 @@
     1.4  
     1.5  abbreviation "le_fun \<equiv> fun_ord leq"
     1.6  abbreviation "lub_fun \<equiv> fun_lub lub"
     1.7 -abbreviation "fixp_fun == ccpo.fixp le_fun lub_fun"
     1.8 +abbreviation "fixp_fun \<equiv> ccpo.fixp le_fun lub_fun"
     1.9  abbreviation "mono_body \<equiv> monotone le_fun leq"
    1.10  abbreviation "admissible \<equiv> ccpo.admissible le_fun lub_fun"
    1.11