deleted redundant proof lines
authorpaulson
Fri May 14 16:50:13 2004 +0200 (2004-05-14)
changeset 147469f7b31cf74d8
parent 14745 94be403deb84
child 14747 2eaff69d3d10
deleted redundant proof lines
src/HOL/Hoare/Pointers0.thy
     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