use "~/ProofGeneral/isa/depends.ML";