[isabelle] Simplification



Dear all,
 
is there any way to erase the following form of
redundant premises in a rule in forward-reasoning?
 
 
I.e., I'd like to have a function of type thm => thm that
converts:
 
[|  A ==> True; B |] ==> C
 
into 
 
B ==> C.
 
(We are talking about HOL.)
 
Best,
 
bu





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