changeset 48891 | c0eafbd55de3 |
parent 46950 | d0181abdbdac |
child 58239 | 1c5bc387bd4c |
--- a/src/HOL/Typedef.thy Wed Aug 22 22:47:16 2012 +0200 +++ b/src/HOL/Typedef.thy Wed Aug 22 22:55:41 2012 +0200 @@ -7,7 +7,6 @@ theory Typedef imports Set keywords "typedef" :: thy_goal and "morphisms" -uses ("Tools/typedef.ML") begin locale type_definition = @@ -109,6 +108,6 @@ end -use "Tools/typedef.ML" setup Typedef.setup +ML_file "Tools/typedef.ML" setup Typedef.setup end