--- a/src/HOL/Predicate_Compile_Examples/Hotel_Example.thy Tue Aug 13 14:20:22 2013 +0200
+++ b/src/HOL/Predicate_Compile_Examples/Hotel_Example.thy Tue Aug 13 16:25:47 2013 +0200
@@ -76,9 +76,9 @@
definition feels_safe :: "event list \<Rightarrow> room \<Rightarrow> bool"
where
- "feels_safe s r = (\<exists>s\<^isub>1 s\<^isub>2 s\<^isub>3 g c c'.
- s = s\<^isub>3 @ [Enter g r c] @ s\<^isub>2 @ [Check_in g r c'] @ s\<^isub>1 \<and>
- no_Check_in (s\<^isub>3 @ s\<^isub>2) r \<and> isin (s\<^isub>2 @ [Check_in g r c] @ s\<^isub>1) r = {})"
+ "feels_safe s r = (\<exists>s\<^sub>1 s\<^sub>2 s\<^sub>3 g c c'.
+ s = s\<^sub>3 @ [Enter g r c] @ s\<^sub>2 @ [Check_in g r c'] @ s\<^sub>1 \<and>
+ no_Check_in (s\<^sub>3 @ s\<^sub>2) r \<and> isin (s\<^sub>2 @ [Check_in g r c] @ s\<^sub>1) r = {})"
section {* Some setup *}