[isabelle] Possible unsoundness in axclass mechanism



theory False = Main:

axclass blurg < type
  blurg: "! x. x ~= x"

lemma l: "(x ~= (x::'a::blurg)) ==> False"
  apply(simp)
  done

lemma "False"
  apply(rule l[of "x"])
  apply(simp only: blurg)
  apply(simp)
  done

end

Is this supposed to happen? I thought declaring an axclass was supposed to be a conservative extension.

T





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