equal
deleted
inserted
replaced
51 apply (simp add: less_SucI) |
51 apply (simp add: less_SucI) |
52 apply (rule transition_is_ex) |
52 apply (rule transition_is_ex) |
53 apply (simp (no_asm) add: spec_ioa_def spec_trans_def trans_of_def) |
53 apply (simp (no_asm) add: spec_ioa_def spec_trans_def trans_of_def) |
54 apply fast |
54 apply fast |
55 txt {* FREE *} |
55 txt {* FREE *} |
56 apply (rule_tac x = " (used - {nat},c) " in exI) |
56 apply (rename_tac nat, rule_tac x = " (used - {nat},c) " in exI) |
57 apply simp |
57 apply simp |
58 apply (rule transition_is_ex) |
58 apply (rule transition_is_ex) |
59 apply (simp (no_asm) add: spec_ioa_def spec_trans_def trans_of_def) |
59 apply (simp (no_asm) add: spec_ioa_def spec_trans_def trans_of_def) |
60 done |
60 done |
61 |
61 |