--- a/src/HOL/Nominal/Examples/CK_Machine.thy Mon Sep 08 14:03:02 2014 +0200
+++ b/src/HOL/Nominal/Examples/CK_Machine.thy Mon Sep 08 14:03:02 2014 +0200
@@ -583,14 +583,5 @@
by (induct \<Gamma>\<equiv>"[]::tctx" t T)
(auto dest!: canonical_tINT intro!: cbv.intros gr0I)
-end
-
-
-
+end
-
-
-
-
-
-