Summary
- added function arg_min
- merged
- added lemma
The file was modified | src/HOL/Lattices_Big.thy (diff) |
The file was modified | src/HOL/Hilbert_Choice.thy (diff) |
The file was modified | src/HOL/Lattices_Big.thy (diff) |
The file was modified | src/HOL/Hilbert_Choice.thy (diff) |