src/Tools/Permanent_Interpretation.thy
changeset 61670 301e0b4ecd45
parent 61669 27ca6147e3b3
child 61671 20d4cd2ceab2
--- a/src/Tools/Permanent_Interpretation.thy	Sat Nov 14 08:45:51 2015 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,14 +0,0 @@
-(*  Title:   Tools/Permanent_Interpretation.thy
-    Author:  Florian Haftmann, TU Muenchen
-*)
-
-section {* Permanent interpretation accompanied with mixin definitions. *}
-
-theory Permanent_Interpretation
-imports Pure
-keywords "defining" and "permanent_interpretation" :: thy_goal
-begin
-
-ML_file "~~/src/Tools/permanent_interpretation.ML"
-
-end