src/HOL/Types_To_Sets/Types_To_Sets.thy
changeset 68428 46beee72fb66
parent 68224 1f7308050349
child 69605 a96320074298
     1.1 --- a/src/HOL/Types_To_Sets/Types_To_Sets.thy	Tue Jun 12 11:18:35 2018 +0100
     1.2 +++ b/src/HOL/Types_To_Sets/Types_To_Sets.thy	Tue Jun 12 16:21:52 2018 +0200
     1.3 @@ -24,4 +24,8 @@
     1.4  text\<open>The following file implements a derived rule that internalizes type class annotations.\<close>
     1.5  ML_file "internalize_sort.ML"
     1.6  
     1.7 +text\<open>The following file provides some automation to unoverload and internalize the parameters o
     1.8 +  the sort constraints of a type variable.\<close>
     1.9 +ML_file \<open>unoverload_type.ML\<close>
    1.10 +
    1.11  end