# HG changeset patch
# User wenzelm
# Date 1399051712 -7200
# Node ID 08041569357ea011245cc26cda505b574647c8cd
# Parent  853f1bcc37551ad7ce9f33a69f2c0c876b1ac4d3
tuned spelling;

diff -r 853f1bcc3755 -r 08041569357e src/HOL/Library/Function_Algebras.thy
--- a/src/HOL/Library/Function_Algebras.thy	Fri May 02 18:54:47 2014 +0200
+++ b/src/HOL/Library/Function_Algebras.thy	Fri May 02 19:28:32 2014 +0200
@@ -176,7 +176,7 @@
 instance "fun" :: (type, ring_char_0) ring_char_0 ..
 
 
-text {* Ordereded structures *}
+text {* Ordered structures *}
 
 instance "fun" :: (type, ordered_ab_semigroup_add) ordered_ab_semigroup_add
   by default (auto simp add: le_fun_def intro: add_left_mono)