diff -r 78dd6bca5627 -r 160d0b08471c thys/Exercises.thy
--- a/thys/Exercises.thy	Fri Jun 30 21:13:40 2017 +0100
+++ b/thys/Exercises.thy	Sat Jul 01 13:08:48 2017 +0100
@@ -2,7 +2,7 @@
   imports Lexer "~~/src/HOL/Library/Infinite_Set"
 begin
 
-section {* some fun tests *}
+section {* Some Fun Facts *}
 
 fun
  zeroable :: "rexp \<Rightarrow> bool"
@@ -16,9 +16,8 @@
 
 lemma zeroable_correctness:
   shows "zeroable r \<longleftrightarrow> L r = {}"
-apply(induct r rule: zeroable.induct)
-apply(auto simp add: Sequ_def)
-done
+by(induct r)(auto simp add: Sequ_def)
+
 
 fun
  atmostempty :: "rexp \<Rightarrow> bool"
@@ -45,22 +44,13 @@
 
 lemma somechars_correctness:
   shows "somechars r \<longleftrightarrow> (\<exists>s. s \<noteq> [] \<and> s \<in> L r)"
-apply(induct r rule: somechars.induct)
-apply(simp)
-apply(simp)
-apply(simp)
-apply(auto)[1]
-prefer 2
-apply(simp)
-apply(rule iffI)
-apply(auto)[1]
-apply (metis Star_decomp neq_Nil_conv)
-apply(rule iffI)
-apply(simp add: Sequ_def zeroable_correctness nullable_correctness)
-apply(auto)[1]
-apply(simp add: Sequ_def zeroable_correctness nullable_correctness)
-apply(auto)[1]
-done
+apply(induct r)
+apply(simp_all add: zeroable_correctness nullable_correctness Sequ_def)
+using Nil_is_append_conv apply blast
+apply blast
+apply(auto)
+using Star_string by fastforce
+
 
 lemma atmostempty_correctness_aux:
   shows "atmostempty r \<longleftrightarrow> \<not> somechars r"
@@ -212,5 +202,6 @@
 using Star_non_empty_string_infinite apply blast
 done
 
+unused_thms
 
 end
\ No newline at end of file