fix typo
Norbert Preining
6 years ago
2587 | 2587 | :parser citp-parse-embed |
2588 | 2588 | :evaluator citp-eval-embed |
2589 | 2589 | :title "`:embed (<label> ... <label>) as <module_name>`" |
2590 | :doc "Icorporate proved goals into the module specified by <module_name> | |
2590 | :doc "Incorporate proved goals into the module specified by <module_name> | |
2591 | 2591 | which will import the current proof context module." |
2592 | 2592 | ) |
2593 | 2593 |