changeset 63167 | 0909deb8059b |
parent 58889 | 5b7a9633cfa8 |
child 67369 | 7360fe6bb423 |
--- a/src/HOL/Nitpick_Examples/Hotel_Nits.thy Thu May 26 16:57:14 2016 +0200 +++ b/src/HOL/Nitpick_Examples/Hotel_Nits.thy Thu May 26 17:51:22 2016 +0200 @@ -5,8 +5,8 @@ Nitpick example based on Tobias Nipkow's hotel key card formalization. *) -section {* Nitpick Example Based on Tobias Nipkow's Hotel Key Card - Formalization *} +section \<open>Nitpick Example Based on Tobias Nipkow's Hotel Key Card + Formalization\<close> theory Hotel_Nits imports Main