| changeset 63167 | 0909deb8059b |
| parent 61076 | bdc1e2f0a86a |
| child 63950 | cdc1e59aa513 |
--- a/src/HOL/Import/HOL_Light_Maps.thy Thu May 26 16:57:14 2016 +0200 +++ b/src/HOL/Import/HOL_Light_Maps.thy Thu May 26 17:51:22 2016 +0200 @@ -5,7 +5,7 @@ Based on earlier code by Steven Obua and Sebastian Skalberg *) -section {* Type and constant mappings of HOL Light importer *} +section \<open>Type and constant mappings of HOL Light importer\<close> theory HOL_Light_Maps imports Import_Setup