src/HOL/Typedef.thy
changeset 47821 b8c7eb0c2f89
parent 42603 996b0c14a430
child 47824 d0181abdbdac
     1.1 --- a/src/HOL/Typedef.thy	Thu Mar 15 17:45:54 2012 +0100
     1.2 +++ b/src/HOL/Typedef.thy	Thu Mar 15 19:02:34 2012 +0100
     1.3 @@ -6,6 +6,7 @@
     1.4  
     1.5  theory Typedef
     1.6  imports Set
     1.7 +keywords "morphisms"
     1.8  uses ("Tools/typedef.ML")
     1.9  begin
    1.10