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