src/HOL/Hoare_Parallel/RG_Hoare.thy
changeset 58860 fee7cfa69c50
parent 55465 0d31c0546286
child 58884 be4d203d35b3
     1.1 --- a/src/HOL/Hoare_Parallel/RG_Hoare.thy	Sat Nov 01 11:40:55 2014 +0100
     1.2 +++ b/src/HOL/Hoare_Parallel/RG_Hoare.thy	Sat Nov 01 14:20:38 2014 +0100
     1.3 @@ -220,7 +220,7 @@
     1.4  apply(force intro:tl_of_cptn_is_cptn)
     1.5  done
     1.6  
     1.7 -lemma Ex_first_occurrence [rule_format]: "P (n::nat) \<longrightarrow> (\<exists>m. P m \<and> (\<forall>i<m. \<not> P i))";
     1.8 +lemma Ex_first_occurrence [rule_format]: "P (n::nat) \<longrightarrow> (\<exists>m. P m \<and> (\<forall>i<m. \<not> P i))"
     1.9  apply(rule nat_less_induct)
    1.10  apply clarify
    1.11  apply(case_tac "\<forall>m. m<n \<longrightarrow> \<not> P m")