diff -r 73127f5db18f -r bea94f1e6771 Closures2.thy
--- a/Closures2.thy	Fri Apr 20 11:27:49 2012 +0000
+++ b/Closures2.thy	Fri Apr 20 11:45:06 2012 +0000
@@ -2,7 +2,6 @@
 imports 
   Closures
   Higman
-  (* "~~/src/HOL/Proofs/Extraction/Higman" *)
 begin
 
 section {* Closure under @{text SUBSEQ} and @{text SUPSEQ} *}
@@ -121,6 +120,7 @@
   show "wf {(x, y). x \<preceq> y \<and> x \<noteq> y}" by (rule wf_subset)
 qed
 
+
 subsection {* Sub- and Supsequences *}
 
 definition