10 votes

How did 'Isabelle' (the theorem prover) get its name?

A little google-fu (and my own memory) tells me it was apparently named by Larry Paulson after Gerard Huet's daughter. Gerard Huet happens to be one of the people behind the less poetically named Coq ...
cody's user avatar
  • 8,114
8 votes

How to understand quantifier without predication " ∀(λφ. (φ x m→ φ y))"?

The $x$ in $\forall x . P(x)$ is not an argument. It is a bound variable indicating which variable the quantifer is ranging over. Let us compare the situation to the definite integral, for concretness ...
Andrej Bauer's user avatar
5 votes

Naming facts exported from blocks in Isabelle/HOL

From section 1.1.2 in the document isar-ref: you can reference facts via explicit name, implicit name and literal position. In this case, the explicit name has not been provided. I believe that the ...
user9716869 - supports Ukraine's user avatar
3 votes

When can the coinduction hypothesis be used?

First, let me recall least and greatest fixed points for $\subseteq$. We are working relative to some set $U$, the universe. In the case of (co)inductive definitions, $U$ is the set of all terms. A ...
kne's user avatar
  • 2,214
3 votes

Difference between $\Rightarrow$, $\Longrightarrow$ and $\rightarrow$ in Isabelle/HOL?

I haven't been able to find a good explanation of how these are different and relate to each other. I know that → is part of HOL and ⇒ and ⟹ part of Isabelle, but it seems that they are basically ...
Alex Nelson's user avatar
1 vote

Isabelle (rule disjE) disjunction elimination rule

Thanks to Patrick Browne I got what I was looking for. ...
Ricardo Boza's user avatar
1 vote

What are the differences between LCF's Theorem and Automath's Prop?

The difference is in what kind of type theorem/Prop is. In Isabelle, theorem is a type in ...
Meven Lennon-Bertrand's user avatar

Only top scored, non community-wiki answers of a minimum length are eligible