Post #2236920

@jonmsterling@mathstodon.xyz I don’t think of Isabelle as being a “pure” LCF prover, because it introduces its own syntax rather than relying on the metalanguage for user documents. This has obvious ergonomic benefits, but I am curious if different choices of metalanguage (and metaprogramming features) than the usual ones made by Poly/ML could improve the base experience so that Isabelle’s approach is unnecessary.