Summary
- made LaTeX happy
- streamlined setup for linear algebra, particularly removed redundant rule declarations
- tuned
- tuned
The file was modified | src/HOL/Fields.thy (diff) |
The file was modified | src/HOL/Fields.thy (diff) |
The file was modified | src/HOL/Int.thy (diff) |
The file was modified | src/HOL/Nat.thy (diff) |
The file was modified | src/HOL/Nonstandard_Analysis/HyperDef.thy (diff) |
The file was modified | src/HOL/Num.thy (diff) |
The file was modified | src/HOL/Numeral_Simprocs.thy (diff) |
The file was modified | src/HOL/Rat.thy (diff) |
The file was modified | src/HOL/Real.thy (diff) |
The file was modified | src/HOL/Tools/int_arith.ML (diff) |
The file was modified | src/HOL/Tools/lin_arith.ML (diff) |
The file was modified | src/HOL/ex/Arith_Examples.thy (diff) |
The file was modified | src/HOL/Library/Float.thy (diff) |
The file was modified | src/HOL/Int.thy (diff) |