Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Summary

  1. merged
  2. lemmas about "card A = 2"; prefer iff to implications
  3. NEWS;
  4. proper sort constraints for strip_shyps, which implicitly performs type instantiation; include solve_constraints in strip_shyps to avoid later conflicts with Thm.transfer;
Changeset 71450:efcd6742ea9c by nipkow:
merged
Changeset 71449:3cf130a896a3 by nipkow:
lemmas about "card A = 2"; prefer iff to implications
The file was modified src/HOL/Analysis/Brouwer_Fixpoint.thy (diff)
The file was modified src/HOL/Finite_Set.thy (diff)
The file was modified src/HOL/Library/Ramsey.thy (diff)
The file was modified src/HOL/Set_Interval.thy (diff)
Changeset 71448:404624eb3a22 by wenzelm:
NEWS;
The file was modified NEWS (diff)
Changeset 71447:439410bf4519 by wenzelm:
proper sort constraints for strip_shyps, which implicitly performs type instantiation;<br>include solve_constraints in strip_shyps to avoid later conflicts with Thm.transfer;
The file was modified src/Pure/thm.ML (diff)