Makarius wrote:
On Thu, 12 Nov 2009, Lucas Dixon wrote:
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
This sort of discussion is analogous to suggesting that we get rid of
and/or/not/implies and write all formulas using the Scheffer stroke
(NAND), or that Gentzen's sequent calculus should be replaced by the
much simpler Hilbert system. It can be done, but who would want to do
it?
Larry
I was really wondering what the principle was that makes -- and ALL
fail (or be inappropriately convoluted) than using the meta-level
connectives: is there a small example that illustrates it?
My own understanding was that the meta-level of Isabelle, and the use of
it by Isar, facilitated the
On Fri, 13 Nov 2009, Lucas Dixon wrote:
I was really wondering what the principle was that makes -- and ALL
fail (or be inappropriately convoluted) than using the meta-level
connectives: is there a small example that illustrates it?
My own understanding was that the meta-level of Isabelle,
On Thu, Nov 12, 2009 at 2:06 PM, Andreas Schropp schropp at in.tum.de wrote:
In a sense, eq_reflection is a meta-thereom, but Pure is not a meta-logic,
so it cannot be proven within the system. ?Thus we need to add it as an
axiom.
But we can prove all instances of the eq_reflection
