`dest`って何？

[2222-42]

why

lemma bcomp_succsに対して、

lemma bcomp_succs:
  "0 ≤ i ⟹
  succs (bcomp b f i) n ⊆ {n .. n + size (bcomp b f i)}
                           ∪ {n + i + size (bcomp b f i)}" 

[dest!]をつけたlemma がある。

lemmas bcomp_succsD [dest!] = bcomp_succs [THEN subsetD, rotated]
(* theorem bcomp_succsD: 
?c ∈ succs (bcomp ?b ?f ?i) ?n ⟹ 
0 ≤ ?i ⟹ 
?c ∈ {?n..?n + size (bcomp ?b ?f ?i)} ∪ {?n + ?i + size (bcomp ?b ?f ?i)} *)

このdestの意味はなにかわからん。

destributionか？ -> destruction

[2222-42]

DefInitSmallの証明の一部にも使われている

http://isabelle.in.tum.de/library/HOL/HOL-IMP/Def_Init_Small.html