src/HOL/Library/Product_Order.thy
changeset 60500 903bb1495239
parent 58881 b9556a055632
child 60580 7e741e22d7fc
     1.1 --- a/src/HOL/Library/Product_Order.thy	Wed Jun 17 10:57:11 2015 +0200
     1.2 +++ b/src/HOL/Library/Product_Order.thy	Wed Jun 17 11:03:05 2015 +0200
     1.3 @@ -2,13 +2,13 @@
     1.4      Author:     Brian Huffman
     1.5  *)
     1.6  
     1.7 -section {* Pointwise order on product types *}
     1.8 +section \<open>Pointwise order on product types\<close>
     1.9  
    1.10  theory Product_Order
    1.11  imports Product_plus Conditionally_Complete_Lattices
    1.12  begin
    1.13  
    1.14 -subsection {* Pointwise ordering *}
    1.15 +subsection \<open>Pointwise ordering\<close>
    1.16  
    1.17  instantiation prod :: (ord, ord) ord
    1.18  begin
    1.19 @@ -52,7 +52,7 @@
    1.20    by default auto
    1.21  
    1.22  
    1.23 -subsection {* Binary infimum and supremum *}
    1.24 +subsection \<open>Binary infimum and supremum\<close>
    1.25  
    1.26  instantiation prod :: (inf, inf) inf
    1.27  begin
    1.28 @@ -103,7 +103,7 @@
    1.29    by default (auto simp add: sup_inf_distrib1)
    1.30  
    1.31  
    1.32 -subsection {* Top and bottom elements *}
    1.33 +subsection \<open>Top and bottom elements\<close>
    1.34  
    1.35  instantiation prod :: (top, top) top
    1.36  begin
    1.37 @@ -155,7 +155,7 @@
    1.38    by default (auto simp add: prod_eqI inf_compl_bot sup_compl_top diff_eq)
    1.39  
    1.40  
    1.41 -subsection {* Complete lattice operations *}
    1.42 +subsection \<open>Complete lattice operations\<close>
    1.43  
    1.44  instantiation prod :: (Inf, Inf) Inf
    1.45  begin
    1.46 @@ -215,8 +215,8 @@
    1.47    unfolding INF_def Inf_prod_def by (simp add: comp_def)
    1.48  
    1.49  
    1.50 -text {* Alternative formulations for set infima and suprema over the product
    1.51 -of two complete lattices: *}
    1.52 +text \<open>Alternative formulations for set infima and suprema over the product
    1.53 +of two complete lattices:\<close>
    1.54  
    1.55  lemma INF_prod_alt_def:
    1.56    "INFIMUM A f = (INFIMUM A (fst o f), INFIMUM A (snd o f))"
    1.57 @@ -227,7 +227,7 @@
    1.58    unfolding SUP_def Sup_prod_def by simp
    1.59  
    1.60  
    1.61 -subsection {* Complete distributive lattices *}
    1.62 +subsection \<open>Complete distributive lattices\<close>
    1.63  
    1.64  (* Contribution: Alessandro Coglio *)
    1.65