src/HOL/Library/Option_ord.thy
changeset 60500 903bb1495239
parent 58881 b9556a055632
child 60679 ade12ef2773c
     1.1 --- a/src/HOL/Library/Option_ord.thy	Wed Jun 17 10:57:11 2015 +0200
     1.2 +++ b/src/HOL/Library/Option_ord.thy	Wed Jun 17 11:03:05 2015 +0200
     1.3 @@ -2,7 +2,7 @@
     1.4      Author:     Florian Haftmann, TU Muenchen
     1.5  *)
     1.6  
     1.7 -section {* Canonical order on option type *}
     1.8 +section \<open>Canonical order on option type\<close>
     1.9  
    1.10  theory Option_ord
    1.11  imports Option Main
    1.12 @@ -104,7 +104,7 @@
    1.13    proof -
    1.14      fix z
    1.15      assume "\<And>x. z = Some x \<Longrightarrow> (P o Some) x"
    1.16 -    with `P None` show "P z" by (cases z) simp_all
    1.17 +    with \<open>P None\<close> show "P z" by (cases z) simp_all
    1.18    qed
    1.19    show "P z" proof (cases z rule: P_Some)
    1.20      case (Some w)
    1.21 @@ -114,7 +114,7 @@
    1.22          fix y :: "'a option"
    1.23          assume "y < Some x"
    1.24          show "P y" proof (cases y rule: P_Some)
    1.25 -          case (Some v) with `y < Some x` have "v < x" by simp
    1.26 +          case (Some v) with \<open>y < Some x\<close> have "v < x" by simp
    1.27            with less show "(P o Some) v" .
    1.28          qed
    1.29        qed