Re: [isabelle] Modify theorem with equality assumption



Am Donnerstag, den 02.04.2015, 18:00 +0200 schrieb Joachim Breitner:
> foo[unfolded eq_thm] or foo[folded eq_thm] do it in Isabelle/Isar; not
> sure about Isabelle/ML.

ignore me, misread your question.

-- 
Dipl.-Math. Dipl.-Inform. Joachim Breitner
Wissenschaftlicher Mitarbeiter
http://pp.ipd.kit.edu/~breitner

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



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