author | berghofe |
Fri, 01 Jul 2005 14:17:32 +0200 | |
changeset 16648 | fc2a425f0977 |
parent 16647 | c6d81ddebb0e |
child 16649 | d88271eb5b26 |
--- 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);