--- a/src/HOL/IMP/Small_Step.thy Tue Feb 13 14:24:50 2018 +0100
+++ b/src/HOL/IMP/Small_Step.thy Thu Feb 15 12:11:00 2018 +0100
@@ -173,7 +173,7 @@
subsection "Final configurations and infinite reductions"
-definition "final cs \<longleftrightarrow> \<not>(EX cs'. cs \<rightarrow> cs')"
+definition "final cs \<longleftrightarrow> \<not>(\<exists>cs'. cs \<rightarrow> cs')"
lemma finalD: "final (c,s) \<Longrightarrow> c = SKIP"
apply(simp add: final_def)
@@ -188,7 +188,7 @@
terminates:\<close>
lemma big_iff_small_termination:
- "(EX t. cs \<Rightarrow> t) \<longleftrightarrow> (EX cs'. cs \<rightarrow>* cs' \<and> final cs')"
+ "(\<exists>t. cs \<Rightarrow> t) \<longleftrightarrow> (\<exists>cs'. cs \<rightarrow>* cs' \<and> final cs')"
by(simp add: big_iff_small final_iff_SKIP)
text\<open>This is the same as saying that the absence of a big step result is