equal
deleted
inserted
replaced
83 |
83 |
84 constdefs |
84 constdefs |
85 WT_bodies :: bool |
85 WT_bodies :: bool |
86 "WT_bodies == !(pn,b):set bodies. WT b" |
86 "WT_bodies == !(pn,b):set bodies. WT b" |
87 |
87 |
88 ML {* use_legacy_bindings (the_context ()) *} |
88 |
|
89 ML {* val make_imp_tac = EVERY'[rtac mp, fn i => atac (i+1), etac thin_rl] *} |
|
90 |
|
91 lemma finite_dom_body: "finite (dom body)" |
|
92 apply (unfold body_def) |
|
93 apply (rule finite_dom_map_of) |
|
94 done |
|
95 |
|
96 lemma WT_bodiesD: "[| WT_bodies; body pn = Some b |] ==> WT b" |
|
97 apply (unfold WT_bodies_def body_def) |
|
98 apply (drule map_of_SomeD) |
|
99 apply fast |
|
100 done |
|
101 |
|
102 declare WTs_elim_cases [elim!] |
89 |
103 |
90 end |
104 end |