src/HOL/Types_To_Sets/Types_To_Sets.thy
changeset 64551 79e9587dbcca
child 68224 1f7308050349
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Types_To_Sets/Types_To_Sets.thy	Mon Dec 12 11:33:14 2016 +0100
     1.3 @@ -0,0 +1,27 @@
     1.4 +(*  Title:      HOL/Types_To_Sets/Types_To_Sets.thy
     1.5 +    Author:     Ondřej Kunčar, TU München
     1.6 +*)
     1.7 +
     1.8 +section \<open>From Types to Sets\<close>
     1.9 +
    1.10 +text \<open>This theory extends Isabelle/HOL's logic by two new inference rules
    1.11 +  to allow translation of types to sets as described in
    1.12 +  O. Kunčar, A. Popescu: From Types to Sets by Local Type Definitions in Higher-Order Logic
    1.13 +  available at http://www21.in.tum.de/~kuncar/documents/kuncar-popescu-t2s2016-extended.pdf.\<close>
    1.14 +
    1.15 +theory Types_To_Sets
    1.16 +  imports Main
    1.17 +begin
    1.18 +
    1.19 +subsection \<open>Rules\<close>
    1.20 +
    1.21 +text\<open>The following file implements the Local Typedef Rule (LT) and extends the logic by the rule.\<close>
    1.22 +ML_file "local_typedef.ML"
    1.23 +
    1.24 +text\<open>The following file implements the Unoverloading Rule (UO) and extends the logic by the rule.\<close>
    1.25 +ML_file "unoverloading.ML"
    1.26 +
    1.27 +text\<open>The following file implements a derived rule that internalizes type class annotations.\<close>
    1.28 +ML_file "internalize_sort.ML"
    1.29 +
    1.30 +end