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