theory Scratch
  imports Pure
begin

ML \<open>
fun sleep_tac t st =
  if Method.detect_closure_state st then Seq.empty
  else (OS.Process.sleep t; Seq.single st);
\<close>

lemma "PROP A"
  apply (tactic \<open>sleep_tac (seconds 0.5) APPEND sleep_tac (seconds 1.0)\<close>)
  back
  oops

end