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

Tobias Nipkow 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? ^^
> Regards,
>  Andy
> _______________________________________________
> Isabelle-dev mailing list
> Isabelle-dev at mailbroy.informatik.tu-muenchen.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

More information about the isabelle-dev mailing list