src/HOL/Types_To_Sets/unoverload_type.ML
16 months ago immler 2018-06-13 result of unoverload is not in normal form
16 months ago immler 2018-06-13 tuned
16 months ago immler 2018-06-13 allow for a list of vars
16 months ago immler 2018-06-13 parse var
16 months ago immler 2018-06-12 tuned
16 months ago immler 2018-06-12 workaround: in internalize_sort, Thm.unconstrainT can rename type variables and therefore invalidate new_tvar
16 months ago immler 2018-06-12 a derived rule combining unoverload and internalize_sort