equal
deleted
inserted
replaced
26 by (Blast_tac 1); |
26 by (Blast_tac 1); |
27 qed_spec_mp "minSet_nonempty"; |
27 qed_spec_mp "minSet_nonempty"; |
28 |
28 |
29 Goal "leadsTo acts (minSet -`` {Some x}) (minSet -`` (Some``greaterThan x))"; |
29 Goal "leadsTo acts (minSet -`` {Some x}) (minSet -`` (Some``greaterThan x))"; |
30 by (rtac leadsTo_weaken 1); |
30 by (rtac leadsTo_weaken 1); |
31 by (rtac ([UC2, UC1] MRS PSP) 1); |
31 by (rtac ([UC2, UC1] MRS psp) 1); |
32 by (ALLGOALS Asm_simp_tac); |
32 by (ALLGOALS Asm_simp_tac); |
33 by (Blast_tac 1); |
33 by (Blast_tac 1); |
34 by Safe_tac; |
34 by Safe_tac; |
35 by (auto_tac (claset() addDs [minSet_eq_SomeD], |
35 by (auto_tac (claset() addDs [minSet_eq_SomeD], |
36 simpset() addsimps [le_def, nat_neq_iff])); |
36 simpset() addsimps [le_def, nat_neq_iff])); |