src/HOL/Orderings.thy
changeset 46884 154dc6ec0041
parent 46882 6242b4bc05bc
child 46950 d0181abdbdac
     1.1 --- a/src/HOL/Orderings.thy	Mon Mar 12 15:12:22 2012 +0100
     1.2 +++ b/src/HOL/Orderings.thy	Mon Mar 12 21:41:11 2012 +0100
     1.3 @@ -1304,7 +1304,7 @@
     1.4    by (simp add: bot_fun_def)
     1.5  
     1.6  instance proof
     1.7 -qed (simp add: le_fun_def bot_apply)
     1.8 +qed (simp add: le_fun_def)
     1.9  
    1.10  end
    1.11  
    1.12 @@ -1320,7 +1320,7 @@
    1.13    by (simp add: top_fun_def)
    1.14  
    1.15  instance proof
    1.16 -qed (simp add: le_fun_def top_apply)
    1.17 +qed (simp add: le_fun_def)
    1.18  
    1.19  end
    1.20