| changeset 61076 | bdc1e2f0a86a |
| parent 60343 | 063698416239 |
| child 61343 | 5b5656a63bd6 |
--- a/src/HOL/ex/FinFunPred.thy Tue Sep 01 17:25:36 2015 +0200 +++ b/src/HOL/ex/FinFunPred.thy Tue Sep 01 22:32:58 2015 +0200 @@ -15,7 +15,7 @@ definition le_finfun_def [code del]: "f \<le> g \<longleftrightarrow> (\<forall>x. f $ x \<le> g $ x)" -definition [code del]: "(f\<Colon>'a \<Rightarrow>f 'b) < g \<longleftrightarrow> f \<le> g \<and> \<not> g \<le> f" +definition [code del]: "(f::'a \<Rightarrow>f 'b) < g \<longleftrightarrow> f \<le> g \<and> \<not> g \<le> f" instance ..