Skip to content
Success

Changes

Summary

  1. made LaTeX happy
  2. streamlined setup for linear algebra, particularly removed redundant rule declarations
  3. tuned
  4. tuned
Changeset 70357:4d0b789e4e21 by haftmann:
made LaTeX happy
The file was modified src/HOL/Fields.thy (diff)
Changeset 70356:4a327c061870 by haftmann:
streamlined setup for linear algebra, particularly removed redundant rule declarations
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)
Changeset 70355:a80ad0ac0837 by haftmann:
tuned
The file was modified src/HOL/Library/Float.thy (diff)
Changeset 70354:9497a6334a26 by haftmann:
tuned
The file was modified src/HOL/Int.thy (diff)