Briefly, x == y was intended to express the definition of x in terms of y. Larry
On 11 Nov 2009, at 21:46, Alexander Krauss wrote: > While we're discussing it: I wonder sometimes what the role of == > was in earlier days of Isabelle. When viewing Pure as the natural > deduction framework to encode my logic, I usually interpret ==> as > the "is derivable from" relation, and !!x as the "this derivation > can be done uniformly for all x". But I have no such clear idea > about ==. Rather I have the feeling that with extensionality, == is > quite strong compared to this... Was it always like this? Or has the > simplifier anything to do with this story?