Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Summary

  1. merged
  2. merged
  3. huge de-apply effort
  4. more uniform Isabelle splash screen -- avoid problems with jEdit splash and Java 11 on some Linux window managers;
  5. yet more de-applying
  6. more de-applying
  7. more tidying up
  8. A bit of de-applying
  9. Algebraic closure: moving more theorems into their rightful places
  10. moving around some material from Algebraic_Closure
  11. merged
  12. full proof of algebraic closure, by Paulo de Vilhena
Changeset 70223:13f8f89f5c41 by paulson:
merged
Changeset 70222:bde8ccb73fd2 by paulson:
merged
Changeset 70221:bca14283e1a8 by paulson _lp15@cam.ac.uk_:
huge de-apply effort
The file was modified src/HOL/Nonstandard_Analysis/NSA.thy (diff)
Changeset 70220:089753519be0 by wenzelm:
more uniform Isabelle splash screen -- avoid problems with jEdit splash and Java 11 on some Linux window managers;
The file was modified Admin/MacOS/Info.plist (diff)
The file was modified Admin/Windows/launch4j/isabelle.xml (diff)
The file was modified src/Tools/jEdit/etc/settings (diff)
The file was modified src/Tools/jEdit/lib/Tools/jedit (diff)
Changeset 70219:b21efbf64292 by paulson _lp15@cam.ac.uk_:
yet more de-applying
The file was modified src/HOL/Nonstandard_Analysis/HyperNat.thy (diff)
The file was modified src/HOL/Nonstandard_Analysis/NatStar.thy (diff)
The file was modified src/HOL/Nonstandard_Analysis/StarDef.thy (diff)
Changeset 70218:e48c0b5897a6 by paulson _lp15@cam.ac.uk_:
more de-applying
The file was modified src/HOL/Nonstandard_Analysis/Star.thy (diff)
Changeset 70217:1f04832cbfcf by paulson _lp15@cam.ac.uk_:
more tidying up
The file was modified src/HOL/Nonstandard_Analysis/HDeriv.thy (diff)
The file was modified src/HOL/Nonstandard_Analysis/NSCA.thy (diff)
Changeset 70216:40f19372a723 by paulson _lp15@cam.ac.uk_:
A bit of de-applying
The file was modified CONTRIBUTORS (diff)
The file was modified src/HOL/Nonstandard_Analysis/HTranscendental.thy (diff)
The file was modified src/HOL/Nonstandard_Analysis/NSCA.thy (diff)
Changeset 70215:8371a25ca177 by paulson _lp15@cam.ac.uk_:
Algebraic closure: moving more theorems into their rightful places
The file was modified NEWS (diff)
The file was modified src/HOL/Algebra/Algebraic_Closure.thy (diff)
The file was modified src/HOL/Algebra/Divisibility.thy (diff)
The file was modified src/HOL/Algebra/Finite_Extensions.thy (diff)
The file was modified src/HOL/Algebra/Ideal.thy (diff)
The file was modified src/HOL/Algebra/Polynomial_Divisibility.thy (diff)
The file was removedsrc/HOL/Algebra/Pred_Zorn.thy
Changeset 70214:58191e01f0b1 by paulson _lp15@cam.ac.uk_:
moving around some material from Algebraic_Closure
The file was modified src/HOL/Algebra/Algebraic_Closure.thy (diff)
The file was modified src/HOL/Algebra/Divisibility.thy (diff)
The file was modified src/HOL/Algebra/Polynomial_Divisibility.thy (diff)
The file was modified src/HOL/Algebra/Ring.thy (diff)
The file was modified src/HOL/Zorn.thy (diff)
Changeset 70213:ff8386fc191d by paulson:
merged
Changeset 70212:e886b58bf698 by paulson _lp15@cam.ac.uk_:
full proof of algebraic closure, by Paulo de Vilhena
The file was modified src/HOL/Algebra/Algebraic_Closure.thy (diff)