Re: [isabelle] Discharging non-atomic assumptions in Isabelle/ML

Hi List,

not sure if it is any better from the point of view of someone who has
experience with ML, but I found this idiom to be quite useful to
discharge assumptions in thm, when I know that the thms in hyp_thms
match its assumptions up to unification:

    val thm' = rule_by_tactic ctxt (EVERY1 (map (single #> solve_tac) hyp_thms)) thm

Maybe this will finally quench my putative thirst for a META_OF :-)


Dipl.-Math. Dipl.-Inform. Joachim Breitner
Wissenschaftlicher Mitarbeiter

Attachment: signature.asc
Description: This is a digitally signed message part

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.