Questions tagged [proof-general]

Proof General is a generic interface for proof assistants based on the Emacs editor. It supports files for several proof assistants including Coq file (.v), an EasyCrypt file (.ec), or a PhoX file (.phx). Historically, other proof assistants such as Isabelle.

Filter by
Sorted by
Tagged with
19 votes
2 answers
381 views

Why is Isabelle usually not just Isabelle but Isabelle/<xyz>?

For most proof assistants the name alone is common, E.g. Coq, Lean but with Isabelle it is often seen as Isabelle/<xyz>? Why the two parts? What is Isabelle/HOL Isabelle/FOL Isabelle/ZF ...
Guy Coder's user avatar
  • 2,836