--- a/src/HOL/BNF/Examples/Derivation_Trees/Gram_Lang.thy Tue Oct 16 18:05:28 2012 +0200
+++ b/src/HOL/BNF/Examples/Derivation_Trees/Gram_Lang.thy Tue Oct 16 18:07:59 2012 +0200
@@ -1356,5 +1356,4 @@
lemma LL_leqv_Lr: "leqv (LL UNIV ts) (Lr UNIV ts)"
using Lr_leqv_L LL_leqv_L by (metis leqv_Sym leqv_trans)
-
end
--- a/src/HOL/BNF/Examples/Derivation_Trees/Parallel.thy Tue Oct 16 18:05:28 2012 +0200
+++ b/src/HOL/BNF/Examples/Derivation_Trees/Parallel.thy Tue Oct 16 18:07:59 2012 +0200
@@ -146,8 +146,4 @@
thus ?thesis by blast
qed
-
-
-
-
end
\ No newline at end of file
--- a/src/HOL/BNF/Examples/Derivation_Trees/Prelim.thy Tue Oct 16 18:05:28 2012 +0200
+++ b/src/HOL/BNF/Examples/Derivation_Trees/Prelim.thy Tue Oct 16 18:07:59 2012 +0200
@@ -62,6 +62,4 @@
shows "A = B"
apply safe using assms apply(case_tac x, auto) by(case_tac x, auto)
-
-
end
\ No newline at end of file