changeset 46799 | f21494dc0bf6 |
parent 42361 | 23f352990944 |
child 46800 | 9696218b02fe |
--- a/src/HOL/Import/import.ML Sat Mar 03 23:49:54 2012 +0100 +++ b/src/HOL/Import/import.ML Sat Mar 03 23:54:44 2012 +0100 @@ -64,7 +64,7 @@ val setup = Method.setup @{binding import} (Scan.lift (Args.name -- Args.name) >> (fn arg => fn ctxt => SIMPLE_METHOD (import_tac ctxt arg))) - "import HOL4 theorem" + "import external theorem" end