src/HOL/Library/Saturated.thy
changeset 60500 903bb1495239
parent 60011 3eef7a43cd51
child 60679 ade12ef2773c
     1.1 --- a/src/HOL/Library/Saturated.thy	Wed Jun 17 10:57:11 2015 +0200
     1.2 +++ b/src/HOL/Library/Saturated.thy	Wed Jun 17 11:03:05 2015 +0200
     1.3 @@ -4,13 +4,13 @@
     1.4      Author:     Florian Haftmann
     1.5  *)
     1.6  
     1.7 -section {* Saturated arithmetic *}
     1.8 +section \<open>Saturated arithmetic\<close>
     1.9  
    1.10  theory Saturated
    1.11  imports Numeral_Type "~~/src/HOL/Word/Type_Length"
    1.12  begin
    1.13  
    1.14 -subsection {* The type of saturated naturals *}
    1.15 +subsection \<open>The type of saturated naturals\<close>
    1.16  
    1.17  typedef ('a::len) sat = "{.. len_of TYPE('a)}"
    1.18    morphisms nat_of Abs_sat
    1.19 @@ -116,7 +116,7 @@
    1.20      proof(cases "c = 0")
    1.21        case True thus ?thesis by (simp add: sat_eq_iff)
    1.22      next
    1.23 -      case False with `a \<noteq> 0` show ?thesis
    1.24 +      case False with \<open>a \<noteq> 0\<close> show ?thesis
    1.25          by (simp add: sat_eq_iff nat_mult_min_left nat_mult_min_right mult.assoc min.assoc min.absorb2)
    1.26      qed
    1.27    qed