diff --git a/thys/Affine_Arithmetic/Print.thy b/thys/Affine_Arithmetic/Print.thy
--- a/thys/Affine_Arithmetic/Print.thy
+++ b/thys/Affine_Arithmetic/Print.thy
@@ -1,234 +1,234 @@
 section \<open>Target Language debug messages\<close>
 theory Print
 imports
   "HOL-Decision_Procs.Approximation"
   Affine_Code
   Show.Show_Instances
   "HOL-Library.Monad_Syntax"
   Optimize_Float
 begin
 
 hide_const (open) floatarith.Max
 
 subsection \<open>Printing\<close>
 
 text \<open>Just for debugging purposes\<close>
 
 definition print::"String.literal \<Rightarrow> unit" where "print x = ()"
 
 context includes integer.lifting begin
 
 end
 
 code_printing constant print \<rightharpoonup> (SML) "TextIO.print"
 
 
 subsection \<open>Write to File\<close>
 
 definition file_output::"String.literal \<Rightarrow> ((String.literal \<Rightarrow> unit) \<Rightarrow> 'a) \<Rightarrow> 'a" where
   "file_output _ f = f (\<lambda>_. ())"
-code_printing constant file_output \<rightharpoonup> (SML) "(fn s => fn f => File.open'_output (fn os => f (File.output os)) (Path.explode s))"
+code_printing constant file_output \<rightharpoonup> (SML) "(fn s => fn f => File'_Stream.open'_output (fn os => f (File'_Stream.output os)) (Path.explode s))"
 
 
 subsection \<open>Show for Floats\<close>
 
 definition showsp_float :: "float showsp"
 where
   "showsp_float p x = (
     let m = mantissa x; e = exponent x in
       if e = 0 then showsp_int p m else showsp_int p m o shows_string ''*2^'' o showsp_int p e)"
 
 lemma show_law_float [show_law_intros]:
   "show_law showsp_float r"
   by (auto simp: showsp_float_def Let_def show_law_simps intro!: show_lawI)
 
 lemma showsp_float_append [show_law_simps]:
   "showsp_float p r (x @ y) = showsp_float p r x @ y"
   by (intro show_lawD show_law_intros)
 
 local_setup \<open>Show_Generator.register_foreign_showsp @{typ float} @{term "showsp_float"} @{thm show_law_float}\<close>
 
 derive "show" float
 
 
 subsection \<open>Convert Float to Decimal number\<close>
 
 text \<open>type for decimal floating point numbers
   (currently just for printing, TODO? generalize theory Float for arbitrary base)\<close>
 
 datatype float10 = Float10 (mantissa10: int) (exponent10: int)
 notation Float10 (infix "\<e>" 999)
 
 partial_function (tailrec) normalize_float10
   where [code]: "normalize_float10 f =
     (if mantissa10 f mod 10 \<noteq> 0 \<or> mantissa10 f = 0 then f
     else normalize_float10 (Float10 (mantissa10 f div 20) (exponent10 f + 1)))"
 
 subsubsection \<open>Version that should be easy to prove correct, but slow!\<close>
 
 context includes floatarith_notation begin
 
 definition "float_to_float10_approximation f = the
   (do {
     let (x, y) = (mantissa f * 1024, exponent f - 10);
     let p = nat (bitlen (abs x) + bitlen (abs y) + 80); \<comment> \<open>FIXME: are there guarantees?\<close>
     y_log \<leftarrow> approx p (Mult (Num (of_int y))
       ((Mult (Ln (Num 2))
         (Inverse (Ln (Num 10)))))) [];
     let e_fl = floor_fl (lower y_log);
     let e = int_floor_fl e_fl;
     m \<leftarrow> approx p (Mult (Num (of_int x)) (Powr (Num 10) (Add(Var 0) (Minus (Num e_fl))))) [Some y_log];
     let ml = lower m;
     let mu = upper m;
     Some (normalize_float10 (Float10 (int_floor_fl ml) e), normalize_float10 (Float10 (- int_floor_fl (- mu)) e))
   })"
 
 end
 
 lemma compute_float_of[code]: "float_of (real_of_float f) = f" by simp
 
 
 subsection \<open>Trusted, but faster version\<close>
 
 text \<open>TODO: this is the HOL version of the SML-code in Approximation.thy\<close>
 
 lemma prod_case_call_mono[partial_function_mono]:
   "mono_tailrec (\<lambda>f. (let (d, e) = a in (\<lambda>y. f (c d e y))) b)"
   by (simp add: split_beta' call_mono)
 
 definition divmod_int::"int \<Rightarrow> int \<Rightarrow> int * int"
 where "divmod_int a b = (a div b, a mod b)"
 
 partial_function (tailrec) f2f10_frac where
  "f2f10_frac c p r digits cnt e =
     (if r = 0 then (digits, cnt, 0)
     else if p = 0 then (digits, cnt, r)
     else (let
       (d, r) = divmod_int (r * 10) (power_int 2 (-e))
     in f2f10_frac (c \<or> d \<noteq> 0) (if d \<noteq> 0 \<or> c then p - 1 else p) r
       (digits * 10 + d) (cnt + 1)) e)"
 declare f2f10_frac.simps[code]
 
 definition float2_float10::"int \<Rightarrow> bool \<Rightarrow> int \<Rightarrow> int \<Rightarrow> (int * int)" where
   "float2_float10 prec rd m e = (
   let
     (m, e) = (if e < 0 then (m,e) else (m * power_int 2 e, 0));
     sgn = sgn m;
     m = abs m;
 
     round_down = (sgn = 1 \<and> rd) \<or> (sgn = -1 \<and> \<not> rd);
 
     (x, r) = divmod_int m ((power_int 2 (-e)));
 
     p = ((if x = 0 then prec else prec - (log2 x + 1)) * 3) div 10 + 1;
 
     (digits, e10, r) = if p > 0 then f2f10_frac (x \<noteq> 0) p r 0 0 e else (0,0,0);
 
     digits = if round_down \<or> r = 0 then digits else digits + 1
 
   in (sgn * (digits + x * (power_int 10 e10)), -e10))"
 
 definition "lfloat10 r = (let f = float_of r in case_prod Float10 (float2_float10 20 True (mantissa f) (exponent f)))"
 definition "ufloat10 r = (let f = float_of r in case_prod Float10 (float2_float10 20 False (mantissa f) (exponent f)))"
 
 partial_function (tailrec) digits
   where [code]: "digits m ds = (if m = 0 then ds else digits (m div 10) (m mod 10 # ds))"
 
 primrec showsp_float10 :: "float10 showsp"
 where
   "showsp_float10 p (Float10 m e) = (
     let
       ds = digits (nat (abs m)) [];
       d = int (length ds);
       e = e + d - 1;
       mp = take 1 ds;
       ms = drop 1 ds;
       ms = rev (dropWhile ((=) 0) (rev ms));
       show_digits = shows_list_gen (showsp_nat p) ''0'' '''' '''' ''''
     in (if m < 0 then shows_string ''-'' else (\<lambda>x. x)) o
         show_digits mp o
         (if ms = [] then (\<lambda>x. x) else shows_string ''.'' o show_digits ms) o
         (if e = 0 then (\<lambda>x. x) else shows_string ''e'' o showsp_int p e))"
 
 lemma show_law_float10_aux:
   fixes m e
   shows "show_law showsp_float10 (Float10 m e)"
   apply (rule show_lawI)
   unfolding showsp_float10.simps Let_def
   apply (simp add: show_law_simps )
   done
 
 lemma show_law_float10 [show_law_intros]: "show_law showsp_float10 r"
   by (cases r) (auto simp: show_law_float10_aux)
 
 lemma showsp_float10_append [show_law_simps]:
   "showsp_float10 p r (x @ y) = showsp_float10 p r x @ y"
   by (intro show_lawD show_law_intros)
 
 local_setup \<open>Show_Generator.register_foreign_showsp @{typ float10} @{term "showsp_float10"} @{thm show_law_float10}\<close>
 
 derive "show" float10
 
 definition "showsp_real p x = showsp_float10 p (lfloat10 x)"
 
 lemma show_law_real[show_law_intros]: "show_law showsp_real x"
   using show_law_float10[of "lfloat10 x"]
   by (auto simp: showsp_real_def[abs_def] Let_def show_law_def
       simp del: showsp_float10.simps intro!: show_law_intros)
 
 local_setup \<open>Show_Generator.register_foreign_showsp @{typ real} @{term "showsp_real"} @{thm show_law_real}\<close>
 derive "show" real
 
 subsection \<open>gnuplot output\<close>
 
 subsubsection \<open>vector output of 2D zonotope\<close>
 
 fun polychain_of_segments::"((real \<times> real) \<times> (real \<times> real)) list \<Rightarrow> (real \<times> real) list"
   where
     "polychain_of_segments [] = []"
   | "polychain_of_segments (((x0, y0), z)#segs) = (x0, y0)#z#map snd segs"
 
 definition shows_segments_of_aform
   where "shows_segments_of_aform a b xs color =
   shows_list_gen id '''' '''' ''\<newline>'' ''\<newline>'' (map (\<lambda>(x0, y0).
       shows_words (map lfloat10 [x0, y0]) o shows_space o shows_string color)
     (polychain_of_segments (segments_of_aform (prod_of_aforms (xs ! a) (xs ! b)))))"
 abbreviation "show_segments_of_aform a b x c \<equiv> shows_segments_of_aform a b x c ''''"
 
 definition shows_box_of_aforms\<comment> \<open>box and some further information\<close>
 where "shows_box_of_aforms (XS::real aform list) = (let
     RS = map (Radius' 20) XS;
     l = map (Inf_aform' 20) XS;
     u = map (Sup_aform' 20) XS
     in shows_words
       (l @ u @ RS) o shows_space o
       shows (card (\<Union>((\<lambda>x. pdevs_domain (snd x)) ` (set XS))))
     )"
 abbreviation "show_box_of_aforms x \<equiv> shows_box_of_aforms x ''''"
 
 definition "pdevs_domains ((XS::real aform list)) = (\<Union>((\<lambda>x. pdevs_domain (snd x)) ` (set XS)))"
 
 definition "generators XS =
     (let
       is = sorted_list_of_set (pdevs_domains XS);
       rs = map (\<lambda>i. (i, map (\<lambda>x. pdevs_apply (snd x) i) XS)) is
     in
       (map fst XS, rs))"
 
 definition shows_box_of_aforms_hr\<comment> \<open>human readable\<close>
 where "shows_box_of_aforms_hr XS = (let
     RS = map (Radius' 20) XS;
     l = map (Inf_aform' 20) XS;
     u = map (Sup_aform' 20) XS
     in shows_paren (shows_words l) o shows_string '' .. '' o shows_paren (shows_words u) o
       shows_string ''; devs: '' o shows (card (pdevs_domains XS)) o
       shows_string ''; tdev: '' o shows_paren (shows_words RS)
     )"
 abbreviation "show_box_of_aforms_hr x \<equiv> shows_box_of_aforms_hr x ''''"
 
 definition shows_aforms_hr\<comment> \<open>human readable\<close>
 where "shows_aforms_hr XS = shows (generators XS)"
 
 abbreviation "show_aform_hr x \<equiv> shows_aforms_hr x ''''"
 
 end
diff --git a/thys/Safe_Distance/Evaluation.thy b/thys/Safe_Distance/Evaluation.thy
--- a/thys/Safe_Distance/Evaluation.thy
+++ b/thys/Safe_Distance/Evaluation.thy
@@ -1,177 +1,177 @@
 \<^marker>\<open>creator "Albert Rizaldi" "Fabian Immler\<close>
 
 section \<open>Evaluation\<close>
 
 theory Evaluation
 imports
   Safe_Distance
   "HOL-Library.Float"
 begin
 
 subsection \<open>Code Generation Setup for Numeric Values\<close>
 
 definition real_div_down :: "nat \<Rightarrow> int \<Rightarrow> int \<Rightarrow> real" where 
   "real_div_down p i j = truncate_down (Suc p) (i / j)"
 
 definition real_div_up :: "nat \<Rightarrow> int \<Rightarrow> int \<Rightarrow> real" where 
   "real_div_up p i j = truncate_up (Suc p) (i / j)"
 
 context includes float.lifting begin
 lift_definition float_div_down :: "nat \<Rightarrow> int \<Rightarrow> int \<Rightarrow> float" is real_div_down
   by (simp add: real_div_down_def)
 
 lift_definition float_div_up :: "nat \<Rightarrow> int \<Rightarrow> int \<Rightarrow> float" is real_div_up
   by (simp add: real_div_up_def)
 end
 
 lemma compute_float_div_up[code]: "float_div_up p i j = - float_div_down p (-i) j"
   including float.lifting
   by transfer (simp add: real_div_up_def real_div_down_def truncate_up_eq_truncate_down)
 
 lemma compute_float_div_down[code]:
   "float_div_down prec m1 m2 = lapprox_rat (Suc prec) m1 m2"
   including float.lifting by transfer (simp add: real_div_down_def)
 
 definition real2_of_real :: "nat \<Rightarrow> real \<Rightarrow> (real * real)" where
   "real2_of_real p x = (truncate_down (Suc p) x, truncate_up (Suc p) x)"
 
 context includes float.lifting begin
 lift_definition float2_of_real :: "nat \<Rightarrow> real \<Rightarrow> float \<times> float" is real2_of_real
   by (auto simp: real2_of_real_def)
 end
 
 definition float2_opt_of_real :: "nat \<Rightarrow> real \<Rightarrow> float interval option" where
   "float2_opt_of_real prec x = Interval' (fst (float2_of_real prec x)) (snd (float2_of_real prec x))"
 
 hide_const (open) Fraction_Field.Fract
 lemma real_of_rat_Fract[simp]: "real_of_rat (Fract a b) = a / b"
   by (simp add: Fract_of_int_quotient of_rat_divide)
 
 lemma [code]: "float2_of_real p (Ratreal r) =
   (let (a, b) = quotient_of r in
   (float_div_down p a b, float_div_up p a b))"
   including float.lifting
   apply transfer
   apply (auto split: prod.split simp: real2_of_real_def real_div_down_def real_div_up_def)
   apply (metis of_rat_divide of_rat_of_int_eq quotient_of_div)+
   done
 
 fun real_of_dec :: "integer \<times> integer \<Rightarrow> real" where
   "real_of_dec (m, e) =
     real_of_int (int_of_integer m) *
       (if e \<ge> 0 then 10 ^ (nat_of_integer e) else inverse (10 ^ (nat (-(int_of_integer e)))))"
 
 lemma "real_of_dec (m, e) = int_of_integer m * 10 powr (int_of_integer e)"
 proof -
   have 1: "e \<ge> 0 \<Longrightarrow> real (nat_of_integer e) = real_of_int (int_of_integer e)"
     using less_eq_integer.rep_eq nat_of_integer.rep_eq by auto
   have 2: "e \<le> 0 \<Longrightarrow> real_of_int (int_of_integer e) = - real (nat (- int_of_integer e))"
     using less_eq_integer.rep_eq by auto
   show ?thesis
     using 1
     apply (auto simp: powr_realpow[symmetric] divide_simps)
     apply (subst (asm) 2)
     apply (auto simp: powr_add[symmetric])
     done
 qed
 
 subsection \<open>Data Evaluation\<close>
 
 definition trans6 where
   "trans6 c chk    se     ve     ae     so     vo     ao =
             chk (c se) (c ve) (c ae) (c so) (c vo) (c ao)"
 
 definition checker_dec where 
   "checker_dec chk p u = 
     trans6 (float2_opt_of_real (nat_of_integer u) o real_of_dec) (chk (nat_of_integer p))"
 
 definition "checker_interval = checker_dec checker'"
 definition "checker_symbolic = trans6 real_of_dec symbolic_checker"
 definition "checker_rational = trans6 real_of_dec checker"
 lemmas[code] = movement.p_def
 
 ML \<open>
   exception InvalidArgument of string;
 
   fun split_string s = String.fields (fn c => c = the (Char.fromString s))
 
   fun dec_of_string s =
     case split_string "." s
     of [r] => (the (IntInf.fromString r), 0)
     | [d1, d2] => (the (IntInf.fromString (d1 ^ d2)), ~ (String.size d2))
     | _ => raise (InvalidArgument s)
 
   fun check_string chk data =
     case split_string "," data of
       [_, so, _, ve, ae, _, vo, ao] => chk data (0, 0)
         (dec_of_string ve) (dec_of_string ae) (dec_of_string so) (dec_of_string vo) (dec_of_string ao)
     | _ => raise (InvalidArgument data)
 \<close>
 
 text \<open>The precision of the input data is roughly 12 and yields similar performance as Sturm\<close>
 
 ML \<open>
 val prec = 12
 
 local
 
 exception Result of int * int;
 
 fun check_line chk n l (y, i) =
   let
     val l = String.substring (l, 0, String.size l - 1)
     val c = check_string chk l
   in if i < n then (if c then y + 1 else y, i + 1) else raise Result (y, i) end
 
 in
 
 fun check_file chk path n =
-  File.fold_lines (check_line chk n) path (0, 0)
+  fold (check_line chk n) (File.read_lines path) (0, 0)
     handle Result res => res;
 
 end
 
 val check_file_symbolic            = check_file (fn _ => \<^code>\<open>checker_symbolic\<close>)
 fun check_file_interval prec uncer = check_file (fn _ => \<^code>\<open>checker_interval\<close> prec uncer)
 val check_file_rational            = check_file (fn _ => \<^code>\<open>checker_rational\<close>)
 \<close>
 
 text \<open>Number of data points:
   \<^item> data01: 1121215
   \<^item> data02: 1341135
   \<^item> data03: 1452656
 \<close>
 
 ML \<open>
   val data01 = \<^master_dir> + \<^path>\<open>data/data01.csv\<close>
   val data02 = \<^master_dir> + \<^path>\<open>data/data02.csv\<close>
   val data03 = \<^master_dir> + \<^path>\<open>data/data03.csv\<close>
 \<close>
 
 ML \<open>
     val t_start1 = Timing.start ();
     val result1 = check_file_rational data01 100;
     val t_end1 = Timing.result t_start1;
     \<^assert> (result1 = (96, 100));
 \<close>
 
 ML \<open>
     val t_start2 = Timing.start ();
     val result2 = check_file_rational data02 100;
     val t_end2 = Timing.result t_start2;
     \<^assert> (result2 = (100, 100));
 \<close>
 
 ML \<open>
     val t_start3 = Timing.start ();
     val result3 = check_file_rational data03 100;
     val t_end3 = Timing.result t_start3;
     \<^assert> (result3 = (76, 100));
 \<close>
 
 text \<open>Precision: 12, Uncertainty: 7 digits\<close>
 ML \<open>\<^assert> (check_file_interval 12 7 data01 100 = (95, 100))\<close>
 ML \<open>\<^assert> (check_file_rational data01 100 = (96, 100))\<close>
 ML \<open>\<^assert> (check_file_symbolic data01 100 = (96, 100))\<close>
 
 end