--- a/src/HOL/Typedef.thy Thu Mar 15 17:45:54 2012 +0100 +++ b/src/HOL/Typedef.thy Thu Mar 15 19:02:34 2012 +0100 @@ -6,6 +6,7 @@ theory Typedef imports Set +keywords "morphisms" uses ("Tools/typedef.ML") begin