equal
deleted
inserted
replaced
1 val make_imp_tac = EVERY'[rtac mp, fn i => atac (i+1), etac thin_rl]; |
1 val make_imp_tac = EVERY'[rtac mp, fn i => atac (i+1), etac thin_rl]; |
2 |
2 |
3 Goalw [body_def] "finite (dom body)"; |
3 Goalw [body_def] "finite (dom body)"; |
4 by (rtac finite_dom_map_of 1); |
4 by (rtac (thm"finite_dom_map_of") 1); |
5 qed "finite_dom_body"; |
5 qed "finite_dom_body"; |
6 |
6 |
7 Goalw [WT_bodies_def, body_def] "[| WT_bodies; body pn = Some b |] ==> WT b"; |
7 Goalw [WT_bodies_def, body_def] "[| WT_bodies; body pn = Some b |] ==> WT b"; |
8 by (dtac map_of_SomeD 1); |
8 by (dtac (thm"map_of_SomeD") 1); |
9 by (Fast_tac 1); |
9 by (Fast_tac 1); |
10 qed "WT_bodiesD"; |
10 qed "WT_bodiesD"; |
11 |
11 |
12 val WTs_elim_cases = map WTs.mk_cases |
12 val WTs_elim_cases = map WTs.mk_cases |
13 ["WT SKIP", "WT (X:==a)", "WT (LOCAL Y:=a IN c)", |
13 ["WT SKIP", "WT (X:==a)", "WT (LOCAL Y:=a IN c)", |