changeset 44890 | 22f665a2e91c |
parent 44241 | 7943b69f0188 |
child 52143 | 36ffe23b25f8 |
--- a/src/HOL/Hoare/Separation.thy Sun Sep 11 22:56:05 2011 +0200 +++ b/src/HOL/Hoare/Separation.thy Mon Sep 12 07:55:43 2011 +0200 @@ -191,7 +191,7 @@ apply vcg apply(simp_all add: star_def ortho_def singl_def) -apply fastsimp +apply fastforce apply (clarsimp simp add:List_non_null) apply(rename_tac ps') @@ -214,7 +214,7 @@ apply(simp) apply fast -apply(fastsimp) +apply(fastforce) done end