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