| changeset 10202 | 9e8b4bebc940 |
| parent 10186 | 499637e8f2c6 |
| 10201:b52140d1a7bc | 10202:9e8b4bebc940 |
|---|---|
44 by (ALLGOALS Full_simp_tac); |
44 by (ALLGOALS Full_simp_tac); |
45 by (ALLGOALS (TRY o Fast_tac)); |
45 by (ALLGOALS (TRY o Fast_tac)); |
46 |
46 |
47 (* while *) |
47 (* while *) |
48 by (strip_tac 1); |
48 by (strip_tac 1); |
49 by (etac (Gamma_mono RSN (2,induct)) 1); |
49 by (etac (Gamma_mono RSN (2,lfp_induct)) 1); |
50 by (rewtac Gamma_def); |
50 by (rewtac Gamma_def); |
51 by (Fast_tac 1); |
51 by (Fast_tac 1); |
52 |
52 |
53 qed_spec_mp "com2"; |
53 qed_spec_mp "com2"; |
54 |
54 |