> 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
