src/HOL/Predicate_Compile_Examples/Hotel_Example.thy
changeset 42463 f270e3e18be5
parent 40104 82873a6f2b81
child 53015 a1119cf551e8
     1.1 --- a/src/HOL/Predicate_Compile_Examples/Hotel_Example.thy	Fri Apr 22 15:57:43 2011 +0200
     1.2 +++ b/src/HOL/Predicate_Compile_Examples/Hotel_Example.thy	Sat Apr 23 13:00:19 2011 +0200
     1.3 @@ -6,7 +6,7 @@
     1.4  datatype key = Key0 | Key1 | Key2 | Key3
     1.5  datatype room = Room0
     1.6  
     1.7 -types card = "key * key"
     1.8 +type_synonym card = "key * key"
     1.9  
    1.10  datatype event =
    1.11     Check_in guest room card | Enter guest room card | Exit guest room