src/Pure/term_sharing.ML
changeset 82648 35e40c60c680
parent 79462 fbdffff89f99