Simplified proof (thanks to strengthened ball_cong).
authorberghofe
Fri, 01 Jul 2005 14:17:32 +0200
changeset 16648 fc2a425f0977
parent 16647 c6d81ddebb0e
child 16649 d88271eb5b26
Simplified proof (thanks to strengthened ball_cong).
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);