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