| changeset 4833 | 2e53109d4bc8 |
| parent 4423 | a129b817b58a |
| 4832:bc11b5b06f87 | 4833:2e53109d4bc8 |
|---|---|
12 by (Simp_tac 1); |
12 by (Simp_tac 1); |
13 by (rtac fix_ind 1); |
13 by (rtac fix_ind 1); |
14 (* simplifier with enhanced adm-tactic: *) |
14 (* simplifier with enhanced adm-tactic: *) |
15 by (Simp_tac 1); |
15 by (Simp_tac 1); |
16 by (Simp_tac 1); |
16 by (Simp_tac 1); |
17 by (simp_tac (simpset() setloop (split_tac[expand_if])) 1); |
17 by (Simp_tac 1); |
18 by (Blast_tac 1); |
18 by (Blast_tac 1); |
19 qed "WHILE_rule_sound"; |
19 qed "WHILE_rule_sound"; |