src/HOL/Types_To_Sets/unoverload_type.ML
Tue, 12 Jun 2018 19:32:42 +0200 immler tuned
Tue, 12 Jun 2018 19:30:55 +0200 immler workaround: in internalize_sort, Thm.unconstrainT can rename type variables and therefore invalidate new_tvar
Tue, 12 Jun 2018 16:21:52 +0200 immler a derived rule combining unoverload and internalize_sort
less more (0) tip