--- 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