# HG changeset patch
# User wenzelm
# Date 1319885734 -7200
# Node ID 3c9f17d017bfd29ff31d16d04c1a11a909db89c3
# Parent  7a97b2bda137a8a0e6e78d73721a6682e41446d5
tuned;

diff -r 7a97b2bda137 -r 3c9f17d017bf src/HOL/Partial_Function.thy
--- 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"