| changeset 45297 | 3c9f17d017bf |
| parent 43082 | 8d0c44de9773 |
| child 46041 | 1e3ff542e83e |
--- 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"