[isabelle] Surprisingly this verifies



The following self-contradictory theory (Two definitions contradict to each other.) verifies by Isabelle 2011. Where is the error?!

theory test
  imports HOL Main
begin

typedecl tag

consts t1::tag
consts t2::tag

definition "f (t1, x) = t1"
definition "f (t1, x) = t2"

end

-- 
Victor Porton - http://portonvictor.org





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