src/HOL/ex/Interpretation_with_Defs.thy

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/ex/Interpretation_with_Defs.thy	Sat Jan 15 20:05:29 2011 +0100
@@ -0,0 +1,12 @@
+(*  Title:      HOL/ex/Interpretation_with_Defs.thy
+    Author:     Florian Haftmann, TU Muenchen
+*)
+
+header {* Interpretation accompanied with mixin definitions.  EXPERIMENTAL. *}
+
+theory Interpretation_with_Defs
+imports Pure
+uses "~~/src/Tools/interpretation_with_defs.ML"
+begin
+
+end