src/HOL/Predicate_Compile_Examples/Hotel_Example.thy
changeset 53015 a1119cf551e8
parent 42463 f270e3e18be5
child 58249 180f1b3508ed
     1.1 --- a/src/HOL/Predicate_Compile_Examples/Hotel_Example.thy	Tue Aug 13 14:20:22 2013 +0200
     1.2 +++ b/src/HOL/Predicate_Compile_Examples/Hotel_Example.thy	Tue Aug 13 16:25:47 2013 +0200
     1.3 @@ -76,9 +76,9 @@
     1.4  
     1.5  definition feels_safe :: "event list \<Rightarrow> room \<Rightarrow> bool"
     1.6  where
     1.7 -  "feels_safe s r = (\<exists>s\<^isub>1 s\<^isub>2 s\<^isub>3 g c c'.
     1.8 -   s = s\<^isub>3 @ [Enter g r c] @ s\<^isub>2 @ [Check_in g r c'] @ s\<^isub>1 \<and>
     1.9 -   no_Check_in (s\<^isub>3 @ s\<^isub>2) r \<and> isin (s\<^isub>2 @ [Check_in g r c] @ s\<^isub>1) r = {})"
    1.10 +  "feels_safe s r = (\<exists>s\<^sub>1 s\<^sub>2 s\<^sub>3 g c c'.
    1.11 +   s = s\<^sub>3 @ [Enter g r c] @ s\<^sub>2 @ [Check_in g r c'] @ s\<^sub>1 \<and>
    1.12 +   no_Check_in (s\<^sub>3 @ s\<^sub>2) r \<and> isin (s\<^sub>2 @ [Check_in g r c] @ s\<^sub>1) r = {})"
    1.13  
    1.14  
    1.15  section {* Some setup *}