tuned language and spelling
authorhaftmann
Thu Oct 23 14:43:48 2014 +0200 (2014-10-23)
changeset 587721df01f0c0589
parent 58771 0997ea62e868
child 58773 1b2e7b78a337
tuned language and spelling
src/HOL/Import/import_data.ML
     1.1 --- a/src/HOL/Import/import_data.ML	Thu Oct 23 14:04:05 2014 +0200
     1.2 +++ b/src/HOL/Import/import_data.ML	Thu Oct 23 14:43:48 2014 +0200
     1.3 @@ -114,7 +114,7 @@
     1.4      (Scan.lift (Parse.name -- Parse.name -- Parse.name) >>
     1.5        (fn ((tyname, absname), repname) => Thm.declaration_attribute
     1.6          (fn th => Context.mapping (add_typ_def tyname absname repname th) I)))
     1.7 -  "declare a type_definion theorem as a map for an imported type abs rep")
     1.8 +  "declare a type_definition theorem as a map for an imported type with abs and rep")
     1.9  
    1.10  val _ =
    1.11    Outer_Syntax.command @{command_spec "import_type_map"}