2013-03-21から1日間の記事一覧
ASM 系のタクティックの負担軽減の為,不要な仮定を消去する目的で作りました.for HOL Light let DEL_TAC n = ASSUM_LIST (fun al-> UNDISCH_THEN ( concl ((el((length al)-1-n)al)) ) (K ALL_TAC) );; for HOL4 fun DEL_TAC n = ASSUM_LIST (fn al => UND…
ASM 系のタクティックの負担軽減の為,不要な仮定を消去する目的で作りました.for HOL Light let DEL_TAC n = ASSUM_LIST (fun al-> UNDISCH_THEN ( concl ((el((length al)-1-n)al)) ) (K ALL_TAC) );; for HOL4 fun DEL_TAC n = ASSUM_LIST (fn al => UND…