src/HOL/Library/Function_Algebras.thy
changeset 56828 08041569357e
parent 54230 b1d955791529
child 58881 b9556a055632
     1.1 --- a/src/HOL/Library/Function_Algebras.thy	Fri May 02 18:54:47 2014 +0200
     1.2 +++ b/src/HOL/Library/Function_Algebras.thy	Fri May 02 19:28:32 2014 +0200
     1.3 @@ -176,7 +176,7 @@
     1.4  instance "fun" :: (type, ring_char_0) ring_char_0 ..
     1.5  
     1.6  
     1.7 -text {* Ordereded structures *}
     1.8 +text {* Ordered structures *}
     1.9  
    1.10  instance "fun" :: (type, ordered_ab_semigroup_add) ordered_ab_semigroup_add
    1.11    by default (auto simp add: le_fun_def intro: add_left_mono)