Summary
- merged
- tuned
- clarified notation: iterated quantifier is negated as one chunk;
- tuned proofs;
- tuned;
- clarified notation;
The file was modified | src/HOL/Num.thy (diff) |
The file was modified | src/HOL/ex/Primrec.thy (diff) |
The file was modified | src/HOL/HOL.thy (diff) |
The file was modified | src/HOL/Rat.thy (diff) |
The file was modified | src/HOL/Hahn_Banach/Subspace.thy (diff) |
The file was modified | NEWS (diff) |
The file was modified | src/HOL/HOL.thy (diff) |