src/HOL/Library/Types_To_Sets.thy
changeset 64551 79e9587dbcca
parent 64550 3e20defb1e3c
child 64552 7aa3c52f27aa
     1.1 --- a/src/HOL/Library/Types_To_Sets.thy	Thu Dec 08 15:11:20 2016 +0100
     1.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.3 @@ -1,27 +0,0 @@
     1.4 -(*  Title:      HOL/Library/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 "Types_To_Sets/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 "Types_To_Sets/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 "Types_To_Sets/internalize_sort.ML"
    1.29 -
    1.30 -end
    1.31 \ No newline at end of file