theory Scratch
  imports Main "HOL-Eisbach.Eisbach_Tools"
begin

notepad
begin
  have a: A1 A2 and b: B1 B2 B3 \<proof>
  from a have C
    using b
  proof (print_fact method_facts)
    show ?thesis \<proof>
  qed
end

end