src/Pure/cterm_items.ML
changeset 82475 0a6d57c4d58b
parent 81959 fae61f1c8113
equal deleted inserted replaced
82474:fcefbef691bf 82475:0a6d57c4d58b