History log of /seL4-l4v-master/isabelle/src/HOL/Types_To_Sets/unoverload_type.ML
Revision Date Author Comments
# 1e239afb 13-May-2019 immler <none@none>

amended to unoverload actually all parameters of a type variable
# 39fbc3fd 18-Jan-2019 immler <none@none>

restore type variable names in unoverload_type

--HG--
extra : rebase_source : 5bebe9c7a6774e498f5c496fcd7ff8b9b932efb0
# ed7a971e 05-Jan-2019 wenzelm <none@none>

isabelle update -u control_cartouches;
# 6571fe8d 13-Jun-2018 immler <none@none>

tuned exception
# d26e0001 13-Jun-2018 immler <none@none>

restructured
# 7ad3a57e 13-Jun-2018 immler <none@none>

result of unoverload is not in normal form
# 97f78e09 13-Jun-2018 immler <none@none>

tuned
# d9bf146d 13-Jun-2018 immler <none@none>

allow for a list of vars
# f2c14c9f 13-Jun-2018 immler <none@none>

parse var
# 81bd1d28 12-Jun-2018 immler <none@none>

tuned
# 81ce9fd6 12-Jun-2018 immler <none@none>

workaround: in internalize_sort, Thm.unconstrainT can rename type variables and therefore invalidate new_tvar
# 9c5e4721 12-Jun-2018 immler <none@none>

a derived rule combining unoverload and internalize_sort