theory Scratch
  imports
    Pure
begin

le mma "x \<equiv> x"
  by (rule ?)+

lemma "x \<equiv> x"
  by (rule ?)+

lemma "x \<equiv> x"
  by (rule ?)+

lemma "x \<equiv> x"
  by (rule ?)+

lemma "x \<equiv> x"
  by (rule ?)+

lemma "x \<equiv> x"
  by (rule ?)+

lemma "x \<equiv> x"
  by (rule ?)+

lemma "x \<equiv> x"
  by (rule ?)+

lemma "x \<equiv> x"
  by (rule ?)+

lemma "x \<equiv> x"
  by (rule ?)+

end