src/HOL/Import/import_rule.ML
changeset 59936 b8ffc3dc9e24
parent 59621 291934bac95e
child 60367 e201bd8973db
     1.1 --- a/src/HOL/Import/import_rule.ML	Mon Apr 06 16:30:44 2015 +0200
     1.2 +++ b/src/HOL/Import/import_rule.ML	Mon Apr 06 17:06:48 2015 +0200
     1.3 @@ -444,7 +444,7 @@
     1.4  fun process_file path thy =
     1.5    (thy, init_state) |> File.fold_lines process_line path |> fst
     1.6  
     1.7 -val _ = Outer_Syntax.command @{command_spec "import_file"}
     1.8 +val _ = Outer_Syntax.command @{command_keyword import_file}
     1.9    "import a recorded proof file"
    1.10    (Parse.path >> (fn name => Toplevel.theory (fn thy => process_file (Path.explode name) thy)))
    1.11