equal
deleted
inserted
replaced
47 Spec.ioa_def,Spec.trans_def,trans_of_def])1); |
47 Spec.ioa_def,Spec.trans_def,trans_of_def])1); |
48 by (Fast_tac 1); |
48 by (Fast_tac 1); |
49 (* FREE *) |
49 (* FREE *) |
50 by (res_inst_tac [("x","(used - {nat},c)")] exI 1); |
50 by (res_inst_tac [("x","(used - {nat},c)")] exI 1); |
51 by (Asm_full_simp_tac 1); |
51 by (Asm_full_simp_tac 1); |
52 by (SELECT_GOAL (safe_tac set_cs) 1); |
|
53 by Auto_tac; |
|
54 by (rtac transition_is_ex 1); |
52 by (rtac transition_is_ex 1); |
55 by (simp_tac (simpset() addsimps [ |
53 by (simp_tac (simpset() addsimps [ |
56 Spec.ioa_def,Spec.trans_def,trans_of_def])1); |
54 Spec.ioa_def,Spec.trans_def,trans_of_def])1); |
57 qed"issimulation"; |
55 qed"issimulation"; |
58 |
56 |