Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Summary

  1. merged
  2. new lemmas, de-applying, etc.
  3. tuned;
  4. merged
  5. discontinued pending_shyps: too much complication due to lazy facts;
  6. proper error;
  7. merged
  8. a few more lemmas from Paulo and Martin
  9. merged
  10. added lemmas
Changeset 68562:1ab1f1681263 by paulson:
merged
Changeset 68561:5e85cda58af6 by paulson _lp15@cam.ac.uk_:
new lemmas, de-applying, etc.
The file was modified src/HOL/Algebra/IntRing.thy (diff)
The file was modified src/HOL/Algebra/Multiplicative_Group.thy (diff)
The file was modified src/HOL/Algebra/Sylow.thy (diff)
Changeset 68560:ad079be4f21c by wenzelm:
tuned;
The file was modified ANNOUNCE (diff)
Changeset 68559:a059271424d0 by wenzelm:
merged
Changeset 68558:7aae213d9e69 by wenzelm:
discontinued pending_shyps: too much complication due to lazy facts;
The file was modified NEWS (diff)
The file was modified src/Doc/Implementation/Logic.thy (diff)
The file was modified src/Pure/Isar/attrib.ML (diff)
The file was modified src/Pure/global_theory.ML (diff)
Changeset 68557:5a836f1b588c by wenzelm:
proper error;
The file was modified src/Pure/Tools/dump.scala (diff)
Changeset 68556:fcffdcb8f506 by paulson:
merged
Changeset 68555:22d51874f37d by paulson _lp15@cam.ac.uk_:
a few more lemmas from Paulo and Martin
The file was modified src/HOL/Algebra/Coset.thy (diff)
The file was modified src/HOL/Algebra/Group.thy (diff)
The file was modified src/HOL/Algebra/Zassenhaus.thy (diff)
Changeset 68554:5273df52ad83 by nipkow:
merged
Changeset 68553:333998becebe by nipkow:
added lemmas
The file was modified src/HOL/Library/Quadratic_Discriminant.thy (diff)