| changeset 61798 | 27f3c10b0b50 |
| parent 61395 | 4f8c2c4a0a8c |
| child 68233 | 5e0e9376b2b0 |
--- a/src/ZF/Bin.thy Mon Dec 07 10:19:30 2015 +0100 +++ b/src/ZF/Bin.thy Mon Dec 07 10:23:50 2015 +0100 @@ -697,7 +697,7 @@ subsection \<open>examples:\<close> -text \<open>@{text combine_numerals_prod} (products of separate literals)\<close> +text \<open>\<open>combine_numerals_prod\<close> (products of separate literals)\<close> lemma "#5 $* x $* #3 = y" apply simp oops schematic_goal "y2 $+ ?x42 = y $+ y2" apply simp oops