src/HOL/Quickcheck_Benchmark/Needham_Schroeder_Base.thy
changeset 58813 625d04d4fd2a
parent 58310 91ea607a34d8
child 61952 546958347e05
equal deleted inserted replaced
58812:5a9a2d3b9f8b 58813:625d04d4fd2a
   192 
   192 
   193 setup {* Predicate_Compile_Data.ignore_consts [@{const_name analz}, @{const_name knows}] *}
   193 setup {* Predicate_Compile_Data.ignore_consts [@{const_name analz}, @{const_name knows}] *}
   194 declare ListMem_iff[symmetric, code_pred_inline]
   194 declare ListMem_iff[symmetric, code_pred_inline]
   195 declare [[quickcheck_timing]]
   195 declare [[quickcheck_timing]]
   196 
   196 
   197 setup {* Exhaustive_Generators.setup_exhaustive_datatype_interpretation *}
   197 setup Exhaustive_Generators.setup_exhaustive_datatype_interpretation
   198 declare [[quickcheck_full_support = false]]
   198 declare [[quickcheck_full_support = false]]
   199 
   199 
   200 end
   200 end