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

[Lucas Dixon]

Makarius wrote:
> Isar depends a lot on Larry's rule calculus !! ==> and in fact makes it
> really shine.  On the other hand, less of this is visible in the text,
> because native structured proof elements take over -- yet another layer
> on top of all that.  Thus Isar is a bit like a rich language like ML,
> where raw lambda abstractions are relatively rare, but notbody would
> think of removing the lambda.
> 
> Plain old HOL will have a hard time imitating Isar without Pure ND
> rules. One would either have to reinvent it, or rethink the whole thing
> from the ground up.
> 
> Again: look at example of Isar calculations, to see where the rule
> framework of Pure comes into place.

this is interesting to me: I don't understand why you couldn't just use
the --> and ALL of HOL to do exactly what ==> and !! are doing? Isn't
that what SPL by Zammit did? The dependencies (in Isabelle, stored in
hyps) can all be recorded outside the logic (as they are in SPL). If
done correctly, like Isar, the final theorems can be re-constructed
easily enough from the recorded structure of the proof text... or so it
seems to me. :)

cheers,
lucas

-- 
The University of Edinburgh is a charitable body, registered in
Scotland, with registration number SC005336.