src/HOL/Predicate_Compile_Examples/Hotel_Example.thy

--- a/src/HOL/Predicate_Compile_Examples/Hotel_Example.thy	Tue Feb 13 14:24:50 2018 +0100
+++ b/src/HOL/Predicate_Compile_Examples/Hotel_Example.thy	Thu Feb 15 12:11:00 2018 +0100
@@ -66,10 +66,10 @@
 primrec hotel :: "event list \<Rightarrow> bool"
 where
   "hotel []  = True"
-| "hotel (e # s) = (hotel s & (case e of
+| "hotel (e # s) = (hotel s \<and> (case e of
   Check_in g r (k,k') \<Rightarrow> k = currk s r \<and> k' \<notin> issued s |
-  Enter g r (k,k') \<Rightarrow> (k,k') : cards s g & (roomk s r : {k, k'}) |
-  Exit g r \<Rightarrow> g : isin s r))"
+  Enter g r (k,k') \<Rightarrow> (k,k') \<in> cards s g \<and> (roomk s r \<in> {k, k'}) |
+  Exit g r \<Rightarrow> g \<in> isin s r))"
 
 definition no_Check_in :: "event list \<Rightarrow> room \<Rightarrow> bool" where(*>*)
 [code del]: "no_Check_in s r \<equiv> \<not>(\<exists>g c. Check_in g r c \<in> set s)"