Skip to main content

Questions tagged [isabelle-hol]

For use with the proof assistant Isabelle with classical higher-order logic.

Filter by
Sorted by
Tagged with
2 votes
0 answers

Disjoint unions in Isabelle/HOL

In mathematics there is a notion of a "disjoint union" in which you "consider" all of the sets to be disjoint even if they are not. For instance, you might want to take the ...
Charles Staats's user avatar
1 vote
1 answer

How to write a low-level proof in Isar?

I would like to formalize ...
Gergely's user avatar
  • 311