--- a/thys/Sulzmann.thy	Thu Aug 16 01:12:00 2018 +0100
+++ b/thys/Sulzmann.thy	Fri Aug 17 12:00:25 2018 +0100
@@ -252,14 +252,10 @@
   apply(simp_all add: retrieve_afuse retrieve_encode_STARS)
   done
 
-
-
-
-
 lemma Q00:
   assumes "s \<in> r \<rightarrow> v"
   shows "\<Turnstile> v : r"
-  using assms
+  using assms 
   apply(induct) 
         apply(auto intro: Prf.intros)
   by (metis Prf.intros(6) Prf_elims(6) insert_iff list.simps(15) val.inject(5))