Without Loss of Generality

Dominique Unruh 🌐

August 30, 2024

Abstract

We introduce a new command wlog in Isabelle/HOL that allows us to (soundly) assume facts without loss of generality inside a proof.

License

BSD License

Topics

Session Wlog