Isabelle é uma ferramenta genérica para provas matemáticas. Ela permite que fórmulas matemáticas sejam expressas em um
idioma formal e fornece ferramentas para provar essas fórmulas em um cálculo lógico.
