Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Isar_examples/MutilatedCheckerboard.thy
changeset 10387 9dac2cad5500
parent 10007 64bf7da1994a
child 10408 d8b3613158b1 
--- a/src/HOL/Isar_examples/MutilatedCheckerboard.thy	Fri Nov 03 21:33:15 2000 +0100
+++ b/src/HOL/Isar_examples/MutilatedCheckerboard.thy	Fri Nov 03 21:33:53 2000 +0100
@@ -223,7 +223,7 @@
       also obtain i j where "?e a b = {(i, j)}"
       proof -
 	have "EX i j. ?e a b = {(i, j)}" by (rule domino_singleton)
-	thus ?thesis by blast
+	thus ?thesis by (blast intro: that)
       qed
       also have "... Un ?e t b = insert (i, j) (?e t b)" by simp
       also have "card ... = Suc (card (?e t b))"
isabelle