src/HOL/Types_To_Sets/Types_To_Sets.thy
author wenzelm
Mon Dec 12 11:33:14 2016 +0100 (20 months ago)
changeset 64551 79e9587dbcca
child 68224 1f7308050349
permissions -rw-r--r--
proper session HOL-Types_To_Sets;
NEWS;
CONTRIBUTORS;
tuned whitespace;
     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