src/HOL/Orderings.thy
changeset 25502 9200b36280c0
parent 25377 dcde128c84a2
child 25510 38c15efe603b
     1.1 --- a/src/HOL/Orderings.thy	Thu Nov 29 07:55:46 2007 +0100
     1.2 +++ b/src/HOL/Orderings.thy	Thu Nov 29 17:08:26 2007 +0100
     1.3 @@ -930,7 +930,7 @@
     1.4  
     1.5  instance bool :: order 
     1.6    le_bool_def: "P \<le> Q \<equiv> P \<longrightarrow> Q"
     1.7 -  less_bool_def: "P < Q \<equiv> P \<le> Q \<and> P \<noteq> Q"
     1.8 +  less_bool_def: "(P\<Colon>bool) < Q \<equiv> P \<le> Q \<and> P \<noteq> Q"
     1.9    by intro_classes (auto simp add: le_bool_def less_bool_def)
    1.10  lemmas [code func del] = le_bool_def less_bool_def
    1.11  
    1.12 @@ -968,7 +968,7 @@
    1.13  
    1.14  instance "fun" :: (type, ord) ord
    1.15    le_fun_def: "f \<le> g \<equiv> \<forall>x. f x \<le> g x"
    1.16 -  less_fun_def: "f < g \<equiv> f \<le> g \<and> f \<noteq> g" ..
    1.17 +  less_fun_def: "(f\<Colon>'a \<Rightarrow> 'b) < g \<equiv> f \<le> g \<and> f \<noteq> g" ..
    1.18  
    1.19  lemmas [code func del] = le_fun_def less_fun_def
    1.20