--- a/progs/Matcher2.thy	Sun Nov 17 19:23:15 2013 +0000
+++ b/progs/Matcher2.thy	Tue Nov 19 23:38:49 2013 +0000
@@ -300,39 +300,4 @@
    (simp_all add: nullable_correctness der_correctness Der_def)
 
 
-
-
-lemma bb: "A \<up> n ;; A\<star> \<subseteq> A\<star>"
-apply(induct n)
-apply(simp)
-apply(simp)
-apply(subst aa[symmetric])
-apply(subst Seq_def)
-apply(auto)
-done
-
-lemma cc: "(\<Union>i\<in>{..n}. A \<up> i) ;; A\<star> \<subseteq> A\<star>"
-apply(induct n)
-apply(simp)
-apply(simp add: Suc_Union del: pow.simps)
-apply(simp only: seq_union)
-apply(rule Un_least)
-defer
-apply(simp)
-apply(rule bb)
-done
-
-lemma "A\<star> ;; A\<star> = A\<star>"
-apply(simp add: Seq_def)
-apply(rule subset_antisym)
-defer
-apply(auto)[1]
-apply(auto simp add: Star_def2)
-
-apply(subst (asm) Star_def2)
-apply(subst (asm) Star_def2)
-apply(auto)
-
-
-
 end    
\ No newline at end of file