theory Scratch
  imports Main
begin

typedef x = \<open>undefined :: nat set\<close>
  (* No proof state shown in "Output" panel (even with "Proof state" and "Auto update" activated). *)
  apply simp
  (* Now proof state is shown *)
  sorry

setup_lifting type_definition_x

lift_definition test :: x is undefined
  (* No proof state shown in "Output" panel (even with "Proof state" and "Auto update" activated). *)
  apply simp
  (* Now proof state is shown *)
  sorry