Summary
- replaced LeastM by arg_min
The file was modified | thys/Buildings/Algebra.thy (diff) |
The file was modified | thys/Buildings/Building.thy (diff) |
The file was modified | thys/Buildings/Chamber.thy (diff) |
The file was modified | thys/Buildings/Coxeter.thy (diff) |
The file was modified | thys/Buildings/Prelim.thy (diff) |
The file was modified | thys/Buildings/Simplicial.thy (diff) |