Questions tagged [isabelle]

Isabelle is an interactive theorem prover, mostly used as Isabelle/HOL which is based on higer-order logic

Filter by
Sorted by
Tagged with
11
votes
1answer
209 views

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

The title says it all, but I'm curious because it isn't obvious how a theorem prover came to be named 'Isabelle'. Was it named for a person? I couldn't find out by some Google searches.
4
votes
1answer
204 views

Proof on tree size using Isabelle

I'm trying to learn a little bit about Isabelle and proofs in general, and it's uses in Programming Language Theory. I'm following a book, "Concrete Semantics with Isabelle/HOL". I'm still in the ...