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

[Tobias Nipkow]

> 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.

Tobias

> 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