src/Doc/Isar_Ref/HOL_Specific.thy

 
     \<^descr>[\<open>random\<close>] The operation @{const Quickcheck_Random.random} of the type
     class @{class random} generates a pseudo-random value of the given size
     and a lazy term reconstruction of the value in the type @{typ
     Code_Evaluation.term}. A pseudo-randomness generator is defined in theory
-    @{theory Random}.
+    @{theory HOL.Random}.
 
     \<^descr>[\<open>narrowing\<close>] implements Haskell's Lazy Smallcheck @{cite
     "runciman-naylor-lindblad"} using the type classes @{class narrowing} and
     @{class partial_term_of}. Variables in the current goal are initially
     represented as symbolic variables. If the execution of the goal tries to

   third argument inherits the allowance of coercsion insertion from the
   position of the constant \<open>c\<close> (policy \<open>0\<close>). The standard usage of policies is
   the definition of syntatic constructs (usually extralogical, i.e., processed
   and stripped during type inference), that should not be destroyed by the
   insertion of coercions (see, for example, the setup for the case syntax in
-  @{theory Ctr_Sugar}).
+  @{theory HOL.Ctr_Sugar}).
 
   \<^descr> @{attribute (HOL) "coercion_enabled"} enables the coercion inference
   algorithm.
 \<close>