diff -r 53fea2ccab19 -r 7beb0cf38292 src/HOL/Library/Parallel.thy --- a/src/HOL/Library/Parallel.thy Thu Jan 02 08:37:52 2025 +0100 +++ b/src/HOL/Library/Parallel.thy Thu Jan 02 08:37:55 2025 +0100 @@ -23,7 +23,7 @@ | constant fork \ (Eval) "Future.fork" | constant join \ (Eval) "Future.join" -code_reserved Eval Future future +code_reserved (Eval) Future future subsection \Parallel lists\ @@ -50,7 +50,7 @@ | constant forall \ (Eval) "Par'_List.forall" | constant exists \ (Eval) "Par'_List.exists" -code_reserved Eval Par_List +code_reserved (Eval) Par_List hide_const (open) fork join map exists forall