--- a/src/HOL/ex/Sudoku.thy Sat Dec 26 15:44:14 2015 +0100
+++ b/src/HOL/ex/Sudoku.thy Sat Dec 26 15:59:27 2015 +0100
@@ -12,9 +12,9 @@
text \<open>
See the paper ``A SAT-based Sudoku Solver'' (Tjark Weber, published at
LPAR'05) for further explanations. (The paper describes an older version of
- this theory that used the model finder @{text refute} to find Sudoku
- solutions. The @{text refute} tool has since been superseded by
- @{text nitpick}, which is used below.)
+ this theory that used the model finder \<open>refute\<close> to find Sudoku
+ solutions. The \<open>refute\<close> tool has since been superseded by
+ \<open>nitpick\<close>, which is used below.)
\<close>
no_notation Groups.one_class.one ("1")