diff -r f58b7f9d3920 -r 3d518b508bbb src/HOL/IMP/ACom.thy
--- a/src/HOL/IMP/ACom.thy	Sat Jan 07 20:44:23 2012 +0100
+++ b/src/HOL/IMP/ACom.thy	Mon Jan 09 11:41:38 2012 +0100
@@ -84,6 +84,14 @@
 lemma strip_anno[simp]: "strip (anno a c) = c"
 by(induct c) simp_all
 
+lemma strip_eq_SKIP:
+  "strip c = com.SKIP \<longleftrightarrow> (EX P. c = SKIP {P})"
+by (cases c) simp_all
+
+lemma strip_eq_Assign:
+  "strip c = x::=e \<longleftrightarrow> (EX P. c = x::=e {P})"
+by (cases c) simp_all
+
 lemma strip_eq_Semi:
   "strip c = c1;c2 \<longleftrightarrow> (EX d1 d2. c = d1;d2 & strip d1 = c1 & strip d2 = c2)"
 by (cases c) simp_all