[isabelle-dev] Isabelle/HOL axiom ext is redundant
nipkow at in.tum.de
Fri Nov 13 00:18:30 CET 2009
> So is the main thing which distinguishes a "logical framework" from a
> "meta logic" the presence of a formal way to do meta-induction (and not
> only prove all cases) and termination checks etc?
What you are thinking of was once called a "meta logical framework" by
David Basin and Bob Constable. Let's not get bogged down in terminology.
You shall know them by their fruits, as the Bible says.
> The funny thing is: Twelf as an implementation of a logical framework
> seems to include these things, so is it actually a meta logic and not a
> logical framework? ^^
> Isabelle-dev mailing list
> Isabelle-dev at mailbroy.informatik.tu-muenchen.de
More information about the isabelle-dev