src/HOL/Import/HOL/ind_type.imp
changeset 37146 f652333bbf8e
parent 14516 a183dec876ab