src/Doc/Locales/Examples3.thy
changeset 63390 c27edca2d827
parent 61732 4653d0835e6e
child 63392 786074d8d61b
equal deleted inserted replaced
63389:5d8607370faf 63390:c27edca2d827
   406   locale non_negative =
   406   locale non_negative =
   407     fixes n :: int
   407     fixes n :: int
   408     assumes non_neg: "0 \<le> n"
   408     assumes non_neg: "0 \<le> n"
   409 
   409 
   410 text \<open>It is again convenient to make the interpretation in an
   410 text \<open>It is again convenient to make the interpretation in an
   411   incremental fashion, first for order preserving maps, the for
   411   incremental fashion, first for order preserving maps, then for
   412   lattice endomorphisms.\<close>
   412   lattice endomorphisms.\<close>
   413 
   413 
   414   sublocale non_negative \<subseteq>
   414   sublocale non_negative \<subseteq>
   415       order_preserving "op \<le>" "op \<le>" "\<lambda>i. n * i"
   415       order_preserving "op \<le>" "op \<le>" "\<lambda>i. n * i"
   416     using non_neg by unfold_locales (rule mult_left_mono)
   416     using non_neg by unfold_locales (rule mult_left_mono)