equal
deleted
inserted
replaced
3 Copyright 2010-2011 |
3 Copyright 2010-2011 |
4 |
4 |
5 Nitpick example based on Tobias Nipkow's hotel key card formalization. |
5 Nitpick example based on Tobias Nipkow's hotel key card formalization. |
6 *) |
6 *) |
7 |
7 |
8 header {* Nitpick Example Based on Tobias Nipkow's Hotel Key Card |
8 section {* Nitpick Example Based on Tobias Nipkow's Hotel Key Card |
9 Formalization *} |
9 Formalization *} |
10 |
10 |
11 theory Hotel_Nits |
11 theory Hotel_Nits |
12 imports Main |
12 imports Main |
13 begin |
13 begin |