# HG changeset patch
# User wenzelm
# Date 1343851949 -7200
# Node ID 053cc8dfde355ec9aa073ce4814005d2cdbe3ac2
# Parent  675988e64bf921bced107052e60ae594b10466d8
fixed document;

diff -r 675988e64bf9 -r 053cc8dfde35 src/HOL/Library/Predicate_Compile_Alternative_Defs.thy
--- a/src/HOL/Library/Predicate_Compile_Alternative_Defs.thy	Wed Aug 01 22:11:54 2012 +0200
+++ b/src/HOL/Library/Predicate_Compile_Alternative_Defs.thy	Wed Aug 01 22:12:29 2012 +0200
@@ -172,7 +172,7 @@
 
 section {* Alternative list definitions *}
 
-subsection {* Alternative rules for length *}
+subsection {* Alternative rules for @{text length} *}
 
 definition size_list :: "'a list => nat"
 where "size_list = size"
@@ -186,7 +186,7 @@
 declare size_list_def[symmetric, code_pred_inline]
 
 
-subsection {* Alternative rules for list_all2 *}
+subsection {* Alternative rules for @{text list_all2} *}
 
 lemma list_all2_NilI [code_pred_intro]: "list_all2 P [] []"
 by auto