Lines Matching defs:t0
378 val (t0,t1) = strip_comb (concl th0)
529 if is_pair t then List.foldl (fn (t0,L0) => L0 @ (strip_pair2 t0)) [] (strip_pair t)
549 val rules = mk_subst_rules (List.map (fn t0 => rhs (concl (REWRITE_CONV [mread_def, toMEM_def, toREG_def, index_of_reg_def] t0))) (strip_pair2 ins));
931 val f = let val t0 = concl (SPEC_ALL th1)
933 let val (assm, t1) = dest_imp t0
935 end handle e => (Term`T`,t0)
953 val f = let val t0 = concl (SPEC_ALL th1)
955 let val (assm, t1) = dest_imp t0
957 end handle e => (Term`T`,t0)
994 val stat1 = let val t0 = concl (SPEC_ALL stat0)
995 in if is_imp t0 then #2 (dest_imp t0) else t0