| changeset 50214 | 67fb9a168d10 |
| parent 49835 | 31f32ec4d766 |
| child 56239 | 17df7145a871 |
--- a/src/HOL/Import/import_rule.ML Mon Nov 26 13:54:43 2012 +0100 +++ b/src/HOL/Import/import_rule.ML Mon Nov 26 14:43:28 2012 +0100 @@ -443,7 +443,7 @@ (thy, init_state) |> File.fold_lines process_line path |> fst val _ = Outer_Syntax.command @{command_spec "import_file"} - "Import a recorded proof file" + "import a recorded proof file" (Parse.path >> (fn name => Toplevel.theory (fn thy => process_file (Path.explode name) thy)))