src/HOL/Tools/Quickcheck/exhaustive_generators.ML
changeset 71394 933ad2385480
parent 70308 7f568724d67e
equal deleted inserted replaced
71391:5556ae257df9 71394:933ad2385480
   441       (\<^term>\<open>If :: bool \<Rightarrow> term list option \<Rightarrow> term list option \<Rightarrow> term list option\<close> $
   441       (\<^term>\<open>If :: bool \<Rightarrow> term list option \<Rightarrow> term list option \<Rightarrow> term list option\<close> $
   442         Bound 0 $ \<^term>\<open>None :: term list option\<close> $ return)
   442         Bound 0 $ \<^term>\<open>None :: term list option\<close> $ return)
   443   in HOLogic.mk_comp (wrap, mk_validator_expr ctxt t) end
   443   in HOLogic.mk_comp (wrap, mk_validator_expr ctxt t) end
   444 
   444 
   445 
   445 
   446 (** generator compiliation **)
   446 (** generator compilation **)
   447 
   447 
   448 structure Data = Proof_Data
   448 structure Data = Proof_Data
   449 (
   449 (
   450   type T =
   450   type T =
   451     (unit -> Code_Numeral.natural -> bool -> Code_Numeral.natural -> (bool * term list) option) *
   451     (unit -> Code_Numeral.natural -> bool -> Code_Numeral.natural -> (bool * term list) option) *