changeset 46950 | d0181abdbdac |
parent 41582 | c34415351b6d |
child 48644 | 70a5d78e8326 |
--- a/src/HOL/ex/Interpretation_with_Defs.thy Thu Mar 15 20:07:00 2012 +0100 +++ b/src/HOL/ex/Interpretation_with_Defs.thy Thu Mar 15 22:08:53 2012 +0100 @@ -6,6 +6,7 @@ theory Interpretation_with_Defs imports Pure +keywords "interpretation" :: thy_goal uses "~~/src/Tools/interpretation_with_defs.ML" begin