src/HOL/Library/Order_Continuity.thy
changeset 61585 a9599d3d7610
parent 60714 ff8aa76d6d1c
child 62373 ea7a442e9a56
     1.1 --- a/src/HOL/Library/Order_Continuity.thy	Thu Nov 05 10:35:37 2015 +0100
     1.2 +++ b/src/HOL/Library/Order_Continuity.thy	Thu Nov 05 10:39:49 2015 +0100
     1.3 @@ -29,8 +29,8 @@
     1.4    done
     1.5  
     1.6  text \<open>
     1.7 -  The name @{text continuous} is already taken in @{text "Complex_Main"}, so we use
     1.8 -  @{text "sup_continuous"} and @{text "inf_continuous"}. These names appear sometimes in literature
     1.9 +  The name \<open>continuous\<close> is already taken in \<open>Complex_Main\<close>, so we use
    1.10 +  \<open>sup_continuous\<close> and \<open>inf_continuous\<close>. These names appear sometimes in literature
    1.11    and have the advantage that these names are duals.
    1.12  \<close>
    1.13