Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Predicate_Compile_Examples/Hotel_Example_Prolog.thy
changeset 67613 ce654b0e6d69
parent 67399 eab6ce8368fa 
--- a/src/HOL/Predicate_Compile_Examples/Hotel_Example_Prolog.thy	Tue Feb 13 14:24:50 2018 +0100
+++ b/src/HOL/Predicate_Compile_Examples/Hotel_Example_Prolog.thy	Thu Feb 15 12:11:00 2018 +0100
@@ -59,11 +59,11 @@
 
 declare List.member_rec[code_pred_def]
 
-lemma [code_pred_def]: "no_Check_in s r = (~ (EX g c. List.member s (Check_in g r c)))"
+lemma [code_pred_def]: "no_Check_in s r = (\<not> (\<exists>g c. List.member s (Check_in g r c)))"
 unfolding no_Check_in_def member_def by auto
 
 lemma [code_pred_def]: "feels_safe s r =
-(EX s\<^sub>1 s\<^sub>2 s\<^sub>3 g c c'.
+(\<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 &
isabelle