diff -r 8bbe2468fedc -r 1612f2a77bf6 thys2/SizeBound4.thy
--- a/thys2/SizeBound4.thy	Sun Jan 30 01:03:26 2022 +0000
+++ b/thys2/SizeBound4.thy	Sun Jan 30 21:21:24 2022 +0000
@@ -146,7 +146,7 @@
 fun retrieve :: "arexp \<Rightarrow> val \<Rightarrow> bit list" where
   "retrieve (AONE bs) Void = bs"
 | "retrieve (ACHAR bs c) (Char d) = bs"
-| "retrieve (AALTs bs [r]) v = bs @ retrieve r v" 
+| "retrieve (AALTs bs [r]) v = bs @ retrieve r v"
 | "retrieve (AALTs bs (r#rs)) (Left v) = bs @ retrieve r v"
 | "retrieve (AALTs bs (r#rs)) (Right v) = bs @ retrieve (AALTs [] rs) v"
 | "retrieve (ASEQ bs r1 r2) (Seq v1 v2) = bs @ retrieve r1 v1 @ retrieve r2 v2"
@@ -457,7 +457,7 @@
      (if (f x) \<in> acc then distinctBy xs f acc 
       else x # (distinctBy xs f ({f x} \<union> acc)))"
 
- 
+  
 
 fun flts :: "arexp list \<Rightarrow> arexp list"
   where