--- a/src/HOL/Isar_Examples/Mutilated_Checkerboard.thy Sat Dec 26 15:03:41 2015 +0100
+++ b/src/HOL/Isar_Examples/Mutilated_Checkerboard.thy Sat Dec 26 15:44:14 2015 +0100
@@ -9,8 +9,10 @@
imports Main
begin
-text \<open>The Mutilated Checker Board Problem, formalized inductively. See @{cite
- "paulson-mutilated-board"} for the original tactic script version.\<close>
+text \<open>
+ The Mutilated Checker Board Problem, formalized inductively. See @{cite
+ "paulson-mutilated-board"} for the original tactic script version.
+\<close>
subsection \<open>Tilings\<close>