--- a/thys/Journal/Paper.thy	Thu Aug 16 01:12:00 2018 +0100
+++ b/thys/Journal/Paper.thy	Fri Aug 17 12:00:25 2018 +0100
@@ -299,7 +299,7 @@
 %@{term "ALT r ZERO"}, @{term "SEQ ONE r"} and @{term "SEQ r ONE"} to
 %@{term r} are applied. 
 
-We extend our results to ???
+We extend our results to ??? Bitcoded version??
 
 *}
 

--- 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))