# HG changeset patch
# User immler
# Date 1538253044 14400
# Node ID 62a0d10386c194a0b082c847470c6af77274fd19
# Parent  6f8ae6ddc26b01e147c57567f068e137b07a2e58
fix (non-existent) document generation

diff -r 6f8ae6ddc26b -r 62a0d10386c1 src/HOL/Types_To_Sets/Examples/Linear_Algebra_On.thy
--- a/src/HOL/Types_To_Sets/Examples/Linear_Algebra_On.thy	Sat Sep 29 23:23:43 2018 +0200
+++ b/src/HOL/Types_To_Sets/Examples/Linear_Algebra_On.thy	Sat Sep 29 16:30:44 2018 -0400
@@ -545,8 +545,9 @@
 text\<open>Get theorem names:\<close>
 print_locale! module
 text\<open>Then replace:
-notes[^"]*"([^"]*).*
-with $1 = module.$1
+\<^verbatim>\<open>notes[^"]*"([^"]*).*\<close>
+with
+\<^verbatim>\<open>$1 = module.$1\<close>
 \<close>
 text \<open>TODO: automate systematic naming!\<close>
 lemmas_with [var_simplified explicit_ab_group_add,
@@ -1173,4 +1174,4 @@
 
 end
 
-end
\ No newline at end of file
+end