src/HOL/Hoare/Pointers0.thy
changeset 14746 9f7b31cf74d8
parent 13771 6cd59cc885a1
child 16417 9bc16273c2d4
     1.1 --- a/src/HOL/Hoare/Pointers0.thy	Fri May 14 16:49:42 2004 +0200
     1.2 +++ b/src/HOL/Hoare/Pointers0.thy	Fri May 14 16:50:13 2004 +0200
     1.3 @@ -384,7 +384,6 @@
     1.4  apply(rule refl)
     1.5  apply (simp add:eq_sym_conv)
     1.6  apply (simp add:eq_sym_conv)
     1.7 -apply (fast)
     1.8  
     1.9  apply(rule conjI)
    1.10  apply clarsimp
    1.11 @@ -403,7 +402,6 @@
    1.12  apply (simp add:eq_sym_conv)
    1.13  apply(rule_tac x = bs in exI)
    1.14  apply (simp add:eq_sym_conv)
    1.15 -apply fast
    1.16  
    1.17  apply(clarsimp simp add:List_app)
    1.18  done