src/Pure/term_sharing.ML
changeset 80738 6adf6cc82013
parent 79462 fbdffff89f99
equal deleted inserted replaced
80737:6984640568b9 80738:6adf6cc82013