Summary
- Replaced some ugly legacy proofs
The file was modified | src/HOL/Auth/NS_Public.thy (diff) |
The file was modified | src/HOL/Auth/NS_Public_Bad.thy (diff) |
The file was modified | src/HOL/Auth/NS_Public.thy (diff) |
The file was modified | src/HOL/Auth/NS_Public_Bad.thy (diff) |