src/HOL/Quickcheck_Random.thy
changeset 81706 7beb0cf38292
parent 72607 feebdaa346e5
--- a/src/HOL/Quickcheck_Random.thy	Thu Jan 02 08:37:52 2025 +0100
+++ b/src/HOL/Quickcheck_Random.thy	Thu Jan 02 08:37:55 2025 +0100
@@ -17,7 +17,8 @@
 code_printing
   constant catch_match \<rightharpoonup> (Quickcheck) "((_) handle Match => _)"
 
-code_reserved Quickcheck Match
+code_reserved
+  (Quickcheck) Match
 
 subsection \<open>The \<open>random\<close> class\<close>
 
@@ -271,7 +272,8 @@
   for this reason we use a distinguished target \<open>Quickcheck\<close>
   not spoiling the regular trusted code generation\<close>
 
-code_reserved Quickcheck Random_Generators
+code_reserved
+  (Quickcheck) Random_Generators
 
 hide_const (open) catch_match random collapse beyond random_fun_aux random_fun_lift