src/Pure/term_sharing.ML
changeset 79425 0875c87b4a4b
parent 77821 d1d28b36ba59
child 79462 fbdffff89f99
equal deleted inserted replaced
79424:16c65e67dd75 79425:0875c87b4a4b