# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1534503625 -3600
# Node ID 9ab8609c66c59c18864fec81731e811e8f72b69e
# Parent  95b3880d428f1cd9263b5068a3046e94328424f0
updated

diff -r 95b3880d428f -r 9ab8609c66c5 thys/Journal/Paper.thy
--- 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??
 
 *}
 
diff -r 95b3880d428f -r 9ab8609c66c5 thys/Sulzmann.thy
--- 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))