src/HOL/Library/FinFun.thy
changeset 61585 a9599d3d7610
parent 61384 9f5145281888
child 61955 e96292f32c3c
     1.1 --- a/src/HOL/Library/FinFun.thy	Thu Nov 05 10:35:37 2015 +0100
     1.2 +++ b/src/HOL/Library/FinFun.thy	Thu Nov 05 10:39:49 2015 +0100
     1.3 @@ -17,7 +17,7 @@
     1.4  \<close>
     1.5  
     1.6  
     1.7 -subsection \<open>The @{text "map_default"} operation\<close>
     1.8 +subsection \<open>The \<open>map_default\<close> operation\<close>
     1.9  
    1.10  definition map_default :: "'b \<Rightarrow> ('a \<rightharpoonup> 'b) \<Rightarrow> 'a \<Rightarrow> 'b"
    1.11  where "map_default b f a \<equiv> case f a of None \<Rightarrow> b | Some b' \<Rightarrow> b'"
    1.12 @@ -307,7 +307,7 @@
    1.13  
    1.14  quickcheck_generator finfun constructors: finfun_update_code, "finfun_const :: 'b \<Rightarrow> 'a \<Rightarrow>f 'b"
    1.15  
    1.16 -subsection \<open>@{text "finfun_update"} as instance of @{text "comp_fun_commute"}\<close>
    1.17 +subsection \<open>\<open>finfun_update\<close> as instance of \<open>comp_fun_commute\<close>\<close>
    1.18  
    1.19  interpretation finfun_update: comp_fun_commute "\<lambda>a f. f(a :: 'a $:= b')"
    1.20    including finfun
    1.21 @@ -1525,7 +1525,7 @@
    1.22  instance by intro_classes (simp add: card_UNIV_finfun_def card_UNIV Let_def card_UNIV_finfun)
    1.23  end
    1.24  
    1.25 -text \<open>Deactivate syntax again. Import theory @{text FinFun_Syntax} to reactivate it again\<close>
    1.26 +text \<open>Deactivate syntax again. Import theory \<open>FinFun_Syntax\<close> to reactivate it again\<close>
    1.27  
    1.28  no_type_notation
    1.29    finfun ("(_ \<Rightarrow>f /_)" [22, 21] 21)