Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Summary

  1. merged
  2. simplified proofs
  3. more rules for ordered real vector spaces
  4. simplified setup
  5. tuned proof
Changeset 70632:f54b19ca9994 by nipkow:
merged
Changeset 70631:f14b997da756 by nipkow:
simplified proofs
The file was modified src/HOL/Data_Structures/List_Ins_Del.thy (diff)
The file was modified src/HOL/Data_Structures/Set_Specs.thy (diff)
Changeset 70630:2402aa499ffe by haftmann:
more rules for ordered real vector spaces
The file was modified src/HOL/Analysis/Elementary_Normed_Spaces.thy (diff)
The file was modified src/HOL/Real_Vector_Spaces.thy (diff)
Changeset 70629:2bbd945728e2 by nipkow:
simplified setup
The file was modified src/HOL/Data_Structures/List_Ins_Del.thy (diff)
Changeset 70628:40b63f2655e8 by nipkow:
tuned proof
The file was modified src/HOL/Data_Structures/Tree234_Set.thy (diff)
The file was modified src/HOL/Data_Structures/Tree23_Set.thy (diff)