changeset 60343 | 063698416239 |
parent 58889 | 5b7a9633cfa8 |
child 61076 | bdc1e2f0a86a |
--- a/src/HOL/ex/FinFunPred.thy Mon Jun 01 18:59:20 2015 +0200 +++ b/src/HOL/ex/FinFunPred.thy Mon Jun 01 18:59:20 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> f \<ge> g" +definition [code del]: "(f\<Colon>'a \<Rightarrow>f 'b) < g \<longleftrightarrow> f \<le> g \<and> \<not> g \<le> f" instance ..