Without Loss of Generality (Q7361253)
From MaRDI portal
!
This is the item page for this Wikibase entity, intended for internal use and editing purposes. Please use the normal view instead:
AFP entry Wlog
| Language | Label | Description | Also known as |
|---|---|---|---|
| default for all languages | No label defined |
||
| English | Without Loss of Generality |
AFP entry Wlog |
Statements
30 August 2024
0 references
Dominique Unruh
0 references
Without Loss of Generality (English)
0 references
We introduce a new command wlog in Isabelle/HOL that allows us to (soundly) assume facts without loss of generality inside a proof.
0 references
