Summary
- add idiom for distinct, non-empty lists
The file was added | thys/Applicative_Lifting/Applicative_DNEList.thy |
The file was modified | thys/Applicative_Lifting/Applicative_Functor.thy (diff) |
The file was added | thys/Applicative_Lifting/Applicative_DNEList.thy |
The file was modified | thys/Applicative_Lifting/Applicative_Functor.thy (diff) |