author | wenzelm |
Fri, 05 May 2006 21:59:41 +0200 | |
changeset 19573 | 340c466c9605 |
parent 17477 | ceb42ea2f223 |
permissions | -rw-r--r-- |
17477 | 1 |
(* $Id$ *) |
2 |
||
8180 | 3 |
val make_imp_tac = EVERY'[rtac mp, fn i => atac (i+1), etac thin_rl]; |
4 |
||
8177 | 5 |
Goalw [body_def] "finite (dom body)"; |
13911 | 6 |
by (rtac (thm"finite_dom_map_of") 1); |
8177 | 7 |
qed "finite_dom_body"; |
8 |
||
9 |
Goalw [WT_bodies_def, body_def] "[| WT_bodies; body pn = Some b |] ==> WT b"; |
|
13911 | 10 |
by (dtac (thm"map_of_SomeD") 1); |
8177 | 11 |
by (Fast_tac 1); |
12 |
qed "WT_bodiesD"; |
|
13 |
||
14 |
AddSEs WTs_elim_cases; |