src/Benchmarks/Quickcheck_Benchmark/Needham_Schroeder_Base.thy

                      (case ev of
                         Says A B X => parts {X} \<union> used evs
                       | Gets A X   => used evs
                       | Notes A X  => parts {X} \<union> used evs)"
 
-subsection {* Preparations for sets *}
+subsection \<open>Preparations for sets\<close>
 
 fun find_first :: "('a => 'b option) => 'a list => 'b option"
 where
   "find_first f [] = None"
 | "find_first f (x # xs) = (case f x of Some y => Some y | None => find_first f xs)"

 
 lemma
   [code]: "neg_cps_of_set (set xs) f i = find_first' f xs"
 sorry
 
-setup {*
+setup \<open>
 let
   val Fun = Predicate_Compile_Aux.Fun
   val Input = Predicate_Compile_Aux.Input
   val Output = Predicate_Compile_Aux.Output
   val Bool = Predicate_Compile_Aux.Bool

  
 in
   Core_Data.force_modes_and_compilations @{const_name Set.member}
     [(oi, (of_set, false)), (ii, (member, false))]
 end
-*}
+\<close>
 
-subsection {* Derived equations for analz, parts and synth *}
+subsection \<open>Derived equations for analz, parts and synth\<close>
 
 lemma [code]:
   "analz H = (let
      H' = H \<union> (\<Union>((%m. case m of \<lbrace>X, Y\<rbrace> => {X, Y} | Crypt K X => if Key (invKey K) : H then {X} else {} | _ => {}) ` H))
    in if H' = H then H else analz H')"

 
 lemmas [code_pred_intro] = synth.intros[folded synth'_def]
 
 code_pred [generator_cps] synth' unfolding synth'_def by (rule synth.cases) fastforce+
 
-setup {* Predicate_Compile_Data.ignore_consts [@{const_name analz}, @{const_name knows}] *}
+setup \<open>Predicate_Compile_Data.ignore_consts [@{const_name analz}, @{const_name knows}]\<close>
 declare ListMem_iff[symmetric, code_pred_inline]
 declare [[quickcheck_timing]]
 
 setup Exhaustive_Generators.setup_exhaustive_datatype_interpretation
 declare [[quickcheck_full_support = false]]