changeset 63167 | 0909deb8059b |
parent 58889 | 5b7a9633cfa8 |
--- a/src/HOL/Import/HOL_Light_Import.thy Thu May 26 16:57:14 2016 +0200 +++ b/src/HOL/Import/HOL_Light_Import.thy Thu May 26 17:51:22 2016 +0200 @@ -3,7 +3,7 @@ Author: Alexander Krauss, QAware GmbH *) -section {* Main HOL Light importer *} +section \<open>Main HOL Light importer\<close> theory HOL_Light_Import imports HOL_Light_Maps