# HG changeset patch
# User wenzelm
# Date 1470156277 -7200
# Node ID a39baba12732707acbc05d3acffc1369e298f72b
# Parent  161c5d8ae266d2ac472cad157ad1993edaccfd46
tuned;

diff -r 161c5d8ae266 -r a39baba12732 src/HOL/Isar_Examples/Knaster_Tarski.thy
--- a/src/HOL/Isar_Examples/Knaster_Tarski.thy	Tue Aug 02 18:13:24 2016 +0200
+++ b/src/HOL/Isar_Examples/Knaster_Tarski.thy	Tue Aug 02 18:44:37 2016 +0200
@@ -7,7 +7,7 @@
 section \<open>Textbook-style reasoning: the Knaster-Tarski Theorem\<close>
 
 theory Knaster_Tarski
-imports Main "~~/src/HOL/Library/Lattice_Syntax"
+  imports Main "~~/src/HOL/Library/Lattice_Syntax"
 begin
 
 
diff -r 161c5d8ae266 -r a39baba12732 src/HOL/Isar_Examples/Mutilated_Checkerboard.thy
--- a/src/HOL/Isar_Examples/Mutilated_Checkerboard.thy	Tue Aug 02 18:13:24 2016 +0200
+++ b/src/HOL/Isar_Examples/Mutilated_Checkerboard.thy	Tue Aug 02 18:44:37 2016 +0200
@@ -6,7 +6,7 @@
 section \<open>The Mutilated Checker Board Problem\<close>
 
 theory Mutilated_Checkerboard
-imports Main
+  imports Main
 begin
 
 text \<open>
@@ -16,11 +16,10 @@
 
 subsection \<open>Tilings\<close>
 
-inductive_set tiling :: "'a set set \<Rightarrow> 'a set set"
-  for A :: "'a set set"
-where
-  empty: "{} \<in> tiling A"
-| Un: "a \<union> t \<in> tiling A" if "a \<in> A" and "t \<in> tiling A" and "a \<subseteq> - t"
+inductive_set tiling :: "'a set set \<Rightarrow> 'a set set" for A :: "'a set set"
+  where
+    empty: "{} \<in> tiling A"
+  | Un: "a \<union> t \<in> tiling A" if "a \<in> A" and "t \<in> tiling A" and "a \<subseteq> - t"
 
 
 text \<open>The union of two disjoint tilings is a tiling.\<close>
@@ -114,9 +113,9 @@
 subsection \<open>Dominoes\<close>
 
 inductive_set domino :: "(nat \<times> nat) set set"
-where
-  horiz: "{(i, j), (i, j + 1)} \<in> domino"
-| vertl: "{(i, j), (i + 1, j)} \<in> domino"
+  where
+    horiz: "{(i, j), (i, j + 1)} \<in> domino"
+  | vertl: "{(i, j), (i + 1, j)} \<in> domino"
 
 lemma dominoes_tile_row:
   "{i} \<times> below (2 * n) \<in> tiling domino"
@@ -242,10 +241,8 @@
 subsection \<open>Main theorem\<close>
 
 definition mutilated_board :: "nat \<Rightarrow> nat \<Rightarrow> (nat \<times> nat) set"
-  where
-    "mutilated_board m n =
-      below (2 * (m + 1)) \<times> below (2 * (n + 1))
-        - {(0, 0)} - {(2 * m + 1, 2 * n + 1)}"
+  where "mutilated_board m n =
+    below (2 * (m + 1)) \<times> below (2 * (n + 1)) - {(0, 0)} - {(2 * m + 1, 2 * n + 1)}"
 
 theorem mutil_not_tiling: "mutilated_board m n \<notin> tiling domino"
 proof (unfold mutilated_board_def)
diff -r 161c5d8ae266 -r a39baba12732 src/HOL/Isar_Examples/Puzzle.thy
--- a/src/HOL/Isar_Examples/Puzzle.thy	Tue Aug 02 18:13:24 2016 +0200
+++ b/src/HOL/Isar_Examples/Puzzle.thy	Tue Aug 02 18:44:37 2016 +0200
@@ -1,7 +1,7 @@
 section \<open>An old chestnut\<close>
 
 theory Puzzle
-imports Main
+  imports Main
 begin
 
 text_raw \<open>\<^footnote>\<open>A question from ``Bundeswettbewerb Mathematik''. Original
diff -r 161c5d8ae266 -r a39baba12732 src/HOL/Isar_Examples/Schroeder_Bernstein.thy
--- a/src/HOL/Isar_Examples/Schroeder_Bernstein.thy	Tue Aug 02 18:13:24 2016 +0200
+++ b/src/HOL/Isar_Examples/Schroeder_Bernstein.thy	Tue Aug 02 18:44:37 2016 +0200
@@ -5,7 +5,7 @@
 section \<open>Schröder-Bernstein Theorem\<close>
 
 theory Schroeder_Bernstein
-imports Main
+  imports Main
 begin
 
 text \<open>
diff -r 161c5d8ae266 -r a39baba12732 src/HOL/Isar_Examples/Structured_Statements.thy
--- a/src/HOL/Isar_Examples/Structured_Statements.thy	Tue Aug 02 18:13:24 2016 +0200
+++ b/src/HOL/Isar_Examples/Structured_Statements.thy	Tue Aug 02 18:44:37 2016 +0200
@@ -5,7 +5,7 @@
 section \<open>Structured statements within Isar proofs\<close>
 
 theory Structured_Statements
-imports Main
+  imports Main
 begin
 
 subsection \<open>Introduction steps\<close>
diff -r 161c5d8ae266 -r a39baba12732 src/HOL/Isar_Examples/Summation.thy
--- a/src/HOL/Isar_Examples/Summation.thy	Tue Aug 02 18:13:24 2016 +0200
+++ b/src/HOL/Isar_Examples/Summation.thy	Tue Aug 02 18:44:37 2016 +0200
@@ -5,7 +5,7 @@
 section \<open>Summing natural numbers\<close>
 
 theory Summation
-imports Main
+  imports Main
 begin
 
 text \<open>