[isabelle-dev] Isabelle/HOL axiom ext is redundant

[Lawrence Paulson]

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?