# HG changeset patch
# User paulson
# Date 1084546213 -7200
# Node ID 9f7b31cf74d8d39a054a83e1942a739e006e48b9
# Parent  94be403deb84a2e9fe902da8ccc9b4e19bab0e91
deleted redundant proof lines

diff -r 94be403deb84 -r 9f7b31cf74d8 src/HOL/Hoare/Pointers0.thy
--- a/src/HOL/Hoare/Pointers0.thy	Fri May 14 16:49:42 2004 +0200
+++ b/src/HOL/Hoare/Pointers0.thy	Fri May 14 16:50:13 2004 +0200
@@ -384,7 +384,6 @@
 apply(rule refl)
 apply (simp add:eq_sym_conv)
 apply (simp add:eq_sym_conv)
-apply (fast)
 
 apply(rule conjI)
 apply clarsimp
@@ -403,7 +402,6 @@
 apply (simp add:eq_sym_conv)
 apply(rule_tac x = bs in exI)
 apply (simp add:eq_sym_conv)
-apply fast
 
 apply(clarsimp simp add:List_app)
 done