equal
deleted
inserted
replaced
|
1 (* Title: HOL/Types_To_Sets/Types_To_Sets.thy |
|
2 Author: Ondřej Kunčar, TU München |
|
3 *) |
|
4 |
|
5 section \<open>From Types to Sets\<close> |
|
6 |
|
7 text \<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 http://www21.in.tum.de/~kuncar/documents/kuncar-popescu-t2s2016-extended.pdf.\<close> |
|
11 |
|
12 theory Types_To_Sets |
|
13 imports Main |
|
14 begin |
|
15 |
|
16 subsection \<open>Rules\<close> |
|
17 |
|
18 text\<open>The following file implements the Local Typedef Rule (LT) and extends the logic by the rule.\<close> |
|
19 ML_file "local_typedef.ML" |
|
20 |
|
21 text\<open>The following file implements the Unoverloading Rule (UO) and extends the logic by the rule.\<close> |
|
22 ML_file "unoverloading.ML" |
|
23 |
|
24 text\<open>The following file implements a derived rule that internalizes type class annotations.\<close> |
|
25 ML_file "internalize_sort.ML" |
|
26 |
|
27 end |