Re: [isabelle] Simplification


The following works for me:

lemma annoyTrue: "(P ==> True) == Trueprop True"
  apply (atomize (full)) by auto

lemma "[| A ==> True ; B |] ==> C"
  apply (simp add: annoyTrue)

proof (prove): step 1

goal (1 subgoal):
 1. B ==> C


Wolff Burkhart wrote:
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
[| 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.