# HG changeset patch
# User berghofe
# Date 1120220252 -7200
# Node ID fc2a425f09779daab3341c0910f7e7f1840237c2
# Parent  c6d81ddebb0e9adfec3357fea8c3b909b6869816
Simplified proof (thanks to strengthened ball_cong).

diff -r c6d81ddebb0e -r fc2a425f0977 src/HOLCF/IOA/Storage/Correctness.ML
--- a/src/HOLCF/IOA/Storage/Correctness.ML	Fri Jul 01 14:16:32 2005 +0200
+++ b/src/HOLCF/IOA/Storage/Correctness.ML	Fri Jul 01 14:17:32 2005 +0200
@@ -49,8 +49,6 @@
 (* FREE *)
 by (res_inst_tac [("x","(used - {nat},c)")] exI 1);
 by (Asm_full_simp_tac 1);
-by (SELECT_GOAL (safe_tac set_cs) 1);
-by Auto_tac;
 by (rtac transition_is_ex 1);
 by (simp_tac (simpset() addsimps [
       Spec.ioa_def,Spec.trans_def,trans_of_def])1);