Share Your Experience: Take the 2024 Developer Survey

# Tag Info

Accepted

### 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 ...
• 8,233
Accepted

### 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 ...
• 30.8k
Accepted

### 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 ...
Accepted

### 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 ...
• 2,254

### 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 ...
• 163
1 vote

### Isabelle (rule disjE) disjunction elimination rule

Thanks to Patrick Browne I got what I was looking for. ...
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 ...

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