changeset 46334 | 3858dc8eabd8 |
parent 46070 | 8392c28d7868 |
child 52019 | a4cbca8f7342 |
--- a/src/HOL/IMP/Collecting1.thy Wed Jan 25 16:07:48 2012 +0100 +++ b/src/HOL/IMP/Collecting1.thy Thu Jan 26 09:52:47 2012 +0100 @@ -11,7 +11,7 @@ lemma step_preserves_le: "\<lbrakk> step S cs = cs; S' \<subseteq> S; cs' \<le> cs \<rbrakk> \<Longrightarrow> step S' cs' \<le> cs" -by (metis mono_step_aux) +by (metis mono2_step) lemma steps_empty_preserves_le: assumes "step S cs = cs" shows "cs' \<le> cs \<Longrightarrow> (step {} ^^ n) cs' \<le> cs"