1(* Title: HOL/Types_To_Sets/Types_To_Sets.thy 2 Author: Ond��ej Kun��ar, TU M��nchen 3*) 4 5section \<open>From Types to Sets\<close> 6 7text \<open>This theory extends Isabelle/HOL's logic by two new inference rules 8 to allow translation of types to sets as described in 9 O. Kun��ar, A. Popescu: From Types to Sets by Local Type Definitions in Higher-Order Logic 10 available at https://www21.in.tum.de/~kuncar/documents/kuncar-popescu-t2s2016-extended.pdf.\<close> 11 12theory Types_To_Sets 13 imports Main 14 keywords "unoverload_definition" :: thy_decl 15begin 16 17subsection \<open>Rules\<close> 18 19text\<open>The following file implements the Local Typedef Rule (LT) and extends the logic by the rule.\<close> 20ML_file \<open>local_typedef.ML\<close> 21 22text\<open>The following file implements the Unoverloading Rule (UO) and extends the logic by the rule.\<close> 23ML_file \<open>unoverloading.ML\<close> 24 25text\<open>The following file implements a derived rule that internalizes type class annotations.\<close> 26ML_file \<open>internalize_sort.ML\<close> 27 28text\<open>The following file provides some automation to unoverload and internalize the parameters of 29 the sort constraints of a type variable.\<close> 30ML_file \<open>unoverload_type.ML\<close> 31 32text \<open>The following file provides automation to define unoverloaded constants from overloaded 33 definitions.\<close> 34named_theorems unoverload_def 35ML_file \<open>unoverload_def.ML\<close> 36 37end 38