src/HOL/Hoare/Pointers0.thy
changeset 17778 93d7e524417a
parent 16417 9bc16273c2d4
child 35101 6ce9177d6b38
     1.1 --- a/src/HOL/Hoare/Pointers0.thy	Fri Oct 07 18:49:20 2005 +0200
     1.2 +++ b/src/HOL/Hoare/Pointers0.thy	Fri Oct 07 20:41:10 2005 +0200
     1.3 @@ -296,9 +296,6 @@
     1.4    {p = X}"
     1.5  apply vcg_simp
     1.6    apply blast
     1.7 - apply clarsimp
     1.8 - apply(erule disjE)
     1.9 -  apply clarsimp
    1.10   apply fastsimp
    1.11  apply clarsimp
    1.12  done