src/HOL/Imperative_HOL/ex/Sublist.thy

--- a/src/HOL/Imperative_HOL/ex/Sublist.thy	Tue Sep 15 15:22:15 2009 +0200
+++ b/src/HOL/Imperative_HOL/ex/Sublist.thy	Tue Sep 15 15:41:23 2009 +0200
@@ -1,4 +1,3 @@
-(* $Id$ *)
 
 header {* Slices of lists *}
 
@@ -6,7 +5,6 @@
 imports Multiset
 begin
 
-
 lemma sublist_split: "i \<le> j \<and> j \<le> k \<Longrightarrow> sublist xs {i..<j} @ sublist xs {j..<k} = sublist xs {i..<k}" 
 apply (induct xs arbitrary: i j k)
 apply simp