2011-11-15から1日間の記事一覧
便利なtheorem-tacticとtheorem-tacticalを幾つか述べます. ■ ASSUME_TAC thmとして仮定を追加する代わりに,LABELTAC_TAC "ラベル" thm とすると,その仮定にラベルが付けられます(というより,LABEL_TAC "" がASSUME_TACの実体です).■ また,結論がimp…
便利なtheorem-tacticとtheorem-tacticalを幾つか述べます. ■ ASSUME_TAC thmとして仮定を追加する代わりに,LABELTAC_TAC "ラベル" thm とすると,その仮定にラベルが付けられます(というより,LABEL_TAC "" がASSUME_TACの実体です).■ また,結論がimp…