| changeset 63167 | 0909deb8059b |
| parent 59669 | de7792ea4090 |
| child 65552 | f533820e7248 |
--- a/src/HOL/Import/Import_Setup.thy Thu May 26 16:57:14 2016 +0200 +++ b/src/HOL/Import/Import_Setup.thy Thu May 26 17:51:22 2016 +0200 @@ -3,7 +3,7 @@ Author: Alexander Krauss, QAware GmbH *) -section {* Importer machinery and required theorems *} +section \<open>Importer machinery and required theorems\<close> theory Import_Setup imports Main "~~/src/HOL/Binomial"