fixed document;
authorwenzelm
Wed Aug 01 22:12:29 2012 +0200 (2012-08-01)
changeset 48640053cc8dfde35
parent 48639 675988e64bf9
child 48641 92b48b8abfe4
child 48651 fb461f81e76e
fixed document;
src/HOL/Library/Predicate_Compile_Alternative_Defs.thy
     1.1 --- a/src/HOL/Library/Predicate_Compile_Alternative_Defs.thy	Wed Aug 01 22:11:54 2012 +0200
     1.2 +++ b/src/HOL/Library/Predicate_Compile_Alternative_Defs.thy	Wed Aug 01 22:12:29 2012 +0200
     1.3 @@ -172,7 +172,7 @@
     1.4  
     1.5  section {* Alternative list definitions *}
     1.6  
     1.7 -subsection {* Alternative rules for length *}
     1.8 +subsection {* Alternative rules for @{text length} *}
     1.9  
    1.10  definition size_list :: "'a list => nat"
    1.11  where "size_list = size"
    1.12 @@ -186,7 +186,7 @@
    1.13  declare size_list_def[symmetric, code_pred_inline]
    1.14  
    1.15  
    1.16 -subsection {* Alternative rules for list_all2 *}
    1.17 +subsection {* Alternative rules for @{text list_all2} *}
    1.18  
    1.19  lemma list_all2_NilI [code_pred_intro]: "list_all2 P [] []"
    1.20  by auto