src/HOL/Library/Predicate_Compile_Alternative_Defs.thy
changeset 61585 a9599d3d7610
parent 61424 c3658c18b7bc
child 62597 b3f2b8c906a6
     1.1 --- a/src/HOL/Library/Predicate_Compile_Alternative_Defs.thy	Thu Nov 05 10:35:37 2015 +0100
     1.2 +++ b/src/HOL/Library/Predicate_Compile_Alternative_Defs.thy	Thu Nov 05 10:39:49 2015 +0100
     1.3 @@ -177,7 +177,7 @@
     1.4  
     1.5  section \<open>Alternative list definitions\<close>
     1.6  
     1.7 -subsection \<open>Alternative rules for @{text length}\<close>
     1.8 +subsection \<open>Alternative rules for \<open>length\<close>\<close>
     1.9  
    1.10  definition size_list' :: "'a list => nat"
    1.11  where "size_list' = size"
    1.12 @@ -191,7 +191,7 @@
    1.13  declare size_list'_def[symmetric, code_pred_inline]
    1.14  
    1.15  
    1.16 -subsection \<open>Alternative rules for @{text list_all2}\<close>
    1.17 +subsection \<open>Alternative rules for \<open>list_all2\<close>\<close>
    1.18  
    1.19  lemma list_all2_NilI [code_pred_intro]: "list_all2 P [] []"
    1.20  by auto