[isabelle] ML "set simp_trace": Congruence Rule question



Hello,

I am examining the simplifier's trace for the following lemma:

lemma "(if A=A then AV else if AA=BB then BV else CV) = AV"
by simp

There is a part of the trace I do not understand - specifically I am talking about the following part:


[1]Applying congruence rule:
A = A == ?c
==> if A = A then AV else if AA = BB then BV else CV ==
   if ?c then AV else if AA = BB then BV else CV

trace_simp_depth_limit exceeded!

Where did the A =A == ?c rule came from?

TIA,
George






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