--- a/src/HOL/Library/Types_To_Sets.thy Sat Dec 10 17:22:47 2016 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,27 +0,0 @@
-(* Title: HOL/Library/Types_To_Sets.thy
- Author: Ondřej Kunčar, TU München
-*)
-
-section \<open>From Types to Sets\<close>
-
-text \<open>This theory extends Isabelle/HOL's logic by two new inference rules
- to allow translation of types to sets as described in
- O. Kunčar, A. Popescu: From Types to Sets by Local Type Definitions in Higher-Order Logic
- available at http://www21.in.tum.de/~kuncar/documents/kuncar-popescu-t2s2016-extended.pdf.\<close>
-
-theory Types_To_Sets
- imports Main
-begin
-
-subsection \<open>Rules\<close>
-
-text\<open>The following file implements the Local Typedef Rule (LT) and extends the logic by the rule.\<close>
-ML_file "Types_To_Sets/local_typedef.ML"
-
-text\<open>The following file implements the Unoverloading Rule (UO) and extends the logic by the rule.\<close>
-ML_file "Types_To_Sets/unoverloading.ML"
-
-text\<open>The following file implements a derived rule that internalizes type class annotations.\<close>
-ML_file "Types_To_Sets/internalize_sort.ML"
-
-end
\ No newline at end of file