changeset 81933 | cb05f8d3fd05 |
parent 81932 | 0a1ed07a458a |
child 81937 | 372ff330a9d9 |
--- a/src/HOL/Import/import_rule.ML Mon Jan 20 22:53:51 2025 +0100 +++ b/src/HOL/Import/import_rule.ML Mon Jan 20 23:00:17 2025 +0100 @@ -1,6 +1,7 @@ (* Title: HOL/Import/import_rule.ML Author: Cezary Kaliszyk, University of Innsbruck Author: Alexander Krauss, QAware GmbH + Author: Makarius Importer proof rules and processing of lines and files.