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:
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
B ==> C.
(We are talking about HOL.)
This archive was generated by a fusion of
Pipermail (Mailman edition) and