src/HOL/Library/Product_Order.thy
changeset 60500 903bb1495239
parent 58881 b9556a055632
child 60580 7e741e22d7fc
--- a/src/HOL/Library/Product_Order.thy	Wed Jun 17 10:57:11 2015 +0200
+++ b/src/HOL/Library/Product_Order.thy	Wed Jun 17 11:03:05 2015 +0200
@@ -2,13 +2,13 @@
     Author:     Brian Huffman
 *)
 
-section {* Pointwise order on product types *}
+section \<open>Pointwise order on product types\<close>
 
 theory Product_Order
 imports Product_plus Conditionally_Complete_Lattices
 begin
 
-subsection {* Pointwise ordering *}
+subsection \<open>Pointwise ordering\<close>
 
 instantiation prod :: (ord, ord) ord
 begin
@@ -52,7 +52,7 @@
   by default auto
 
 
-subsection {* Binary infimum and supremum *}
+subsection \<open>Binary infimum and supremum\<close>
 
 instantiation prod :: (inf, inf) inf
 begin
@@ -103,7 +103,7 @@
   by default (auto simp add: sup_inf_distrib1)
 
 
-subsection {* Top and bottom elements *}
+subsection \<open>Top and bottom elements\<close>
 
 instantiation prod :: (top, top) top
 begin
@@ -155,7 +155,7 @@
   by default (auto simp add: prod_eqI inf_compl_bot sup_compl_top diff_eq)
 
 
-subsection {* Complete lattice operations *}
+subsection \<open>Complete lattice operations\<close>
 
 instantiation prod :: (Inf, Inf) Inf
 begin
@@ -215,8 +215,8 @@
   unfolding INF_def Inf_prod_def by (simp add: comp_def)
 
 
-text {* Alternative formulations for set infima and suprema over the product
-of two complete lattices: *}
+text \<open>Alternative formulations for set infima and suprema over the product
+of two complete lattices:\<close>
 
 lemma INF_prod_alt_def:
   "INFIMUM A f = (INFIMUM A (fst o f), INFIMUM A (snd o f))"
@@ -227,7 +227,7 @@
   unfolding SUP_def Sup_prod_def by simp
 
 
-subsection {* Complete distributive lattices *}
+subsection \<open>Complete distributive lattices\<close>
 
 (* Contribution: Alessandro Coglio *)