tuned;

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