Questions tagged [isabelle]

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

11
votes
1answer
206 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
200 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 ...