--- a/src/HOL/Import/import_data.ML Thu Oct 23 14:04:05 2014 +0200
+++ b/src/HOL/Import/import_data.ML Thu Oct 23 14:43:48 2014 +0200
@@ -114,7 +114,7 @@
(Scan.lift (Parse.name -- Parse.name -- Parse.name) >>
(fn ((tyname, absname), repname) => Thm.declaration_attribute
(fn th => Context.mapping (add_typ_def tyname absname repname th) I)))
- "declare a type_definion theorem as a map for an imported type abs rep")
+ "declare a type_definition theorem as a map for an imported type with abs and rep")
val _ =
Outer_Syntax.command @{command_spec "import_type_map"}