Skip to content
Success

Changes

Summary

  1. Merged
  2. Removed some uses of deprecated _tac methods. (Patch from Viorel Preoteasa)
  3. Added some simple facts about limits
  4. added lemmas
Changeset 67951:655aa11359dc by manuel eberl _eberlm@in.tum.de_:
Removed some uses of deprecated _tac methods. (Patch from Viorel Preoteasa)
The file was modified src/HOL/Enum.thy (diff)
The file was modified src/HOL/Hilbert_Choice.thy (diff)
The file was modified src/HOL/Library/Option_ord.thy (diff)
The file was modified src/HOL/Predicate.thy (diff)
Changeset 67950:99eaa5cedbb7 by manuel eberl _eberlm@in.tum.de_:
Added some simple facts about limits
The file was modified src/HOL/Filter.thy (diff)
The file was modified src/HOL/Limits.thy (diff)
The file was modified src/HOL/Topological_Spaces.thy (diff)
Changeset 67949:4bb49ed64933 by nipkow:
added lemmas
The file was modified src/HOL/List.thy (diff)