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