theory Scratch
  imports Pure
begin

ML \<open>
  val ZF_ctxt = Proof_Context.init_global (Thy_Info.get_theory "ZFC");
  val ZF_prop = Syntax.read_prop ZF_ctxt "x = x";

  val HOL_ctxt = Proof_Context.init_global (Thy_Info.get_theory "Main");
  val HOL_thm =
    Goal.prove HOL_ctxt
      ["x", "y"]
      [Syntax.read_prop HOL_ctxt "(x::'a) = y"]
      (Syntax.read_prop HOL_ctxt "(y::'a) = x")
      (fn {context = goal_ctxt, prems} =>
        resolve_tac goal_ctxt (Proof_Context.get_thms goal_ctxt "sym") 1 THEN
        resolve_tac goal_ctxt prems 1);
\<close>

end