src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML
changeset 50093 a2886be4d615
parent 50057 57209cfbf16b
child 51126 df86080de4cb
equal deleted inserted replaced
50092:39898c719339 50093:a2886be4d615
    33 structure Predicate_Compile_Quickcheck : PREDICATE_COMPILE_QUICKCHECK =
    33 structure Predicate_Compile_Quickcheck : PREDICATE_COMPILE_QUICKCHECK =
    34 struct
    34 struct
    35 
    35 
    36 open Predicate_Compile_Aux;
    36 open Predicate_Compile_Aux;
    37 
    37 
    38 type seed = Random_Engine.seed:
    38 type seed = Random_Engine.seed;
    39 
    39 
    40 (* FIXME just one data slot (record) per program unit *)
    40 (* FIXME just one data slot (record) per program unit *)
    41 
    41 
    42 structure Pred_Result = Proof_Data
    42 structure Pred_Result = Proof_Data
    43 (
    43 (