Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Summary

  1. back to build_polyml_component according to 54c6ec4166a4 (amending 808e6ddb5a50);
  2. reactivated unfinished tool (cf. a3a847c4fbdb);
  3. tuned whitespace;
  4. clarified meta_digest;
  5. tuned;
  6. added isablle build option -f;
  7. canonical multiplicative euclidean size
  8. clarified parity
  9. clarified uniqueness criterion for euclidean rings
  10. tuned proofs
  11. tuned imports
Changeset 66846:c04f46a6f29d by wenzelm:
back to build_polyml_component according to 54c6ec4166a4 (amending 808e6ddb5a50);
The file was modified Admin/polyml/CHECKLIST (diff)
Changeset 66845:6847eb01ae47 by wenzelm:
reactivated unfinished tool (cf. a3a847c4fbdb);
The file was modified src/Pure/System/isabelle_tool.scala (diff)
Changeset 66844:0746d4781674 by wenzelm:
tuned whitespace;
The file was modified NEWS (diff)
Changeset 66843:be08a7691c62 by wenzelm:
clarified meta_digest;
The file was modified NEWS (diff)
The file was modified src/Pure/Thy/sessions.scala (diff)
Changeset 66842:7ded55dd2a55 by wenzelm:
tuned;
The file was modified src/HOL/ROOT (diff)
Changeset 66841:5c32a072ca8b by wenzelm:
added isablle build option -f;
The file was modified NEWS (diff)
The file was modified src/Doc/System/Sessions.thy (diff)
The file was modified src/Pure/Tools/build.scala (diff)
Changeset 66840:0d689d71dbdc by haftmann:
canonical multiplicative euclidean size
The file was modified src/HOL/Computational_Algebra/Polynomial_Factorial.thy (diff)
The file was modified src/HOL/Euclidean_Division.thy (diff)
The file was modified src/HOL/Parity.thy (diff)
Changeset 66839:909ba5ed93dd by haftmann:
clarified parity
The file was modified src/HOL/Code_Numeral.thy (diff)
The file was modified src/HOL/Euclidean_Division.thy (diff)
The file was modified src/HOL/Parity.thy (diff)
Changeset 66838:17989f6bc7b2 by haftmann:
clarified uniqueness criterion for euclidean rings
The file was modified src/HOL/Code_Numeral.thy (diff)
The file was modified src/HOL/Computational_Algebra/Field_as_Ring.thy (diff)
The file was modified src/HOL/Computational_Algebra/Polynomial_Factorial.thy (diff)
The file was modified src/HOL/Enum.thy (diff)
The file was modified src/HOL/Euclidean_Division.thy (diff)
Changeset 66837:6ba663ff2b1c by haftmann:
tuned proofs
The file was modified src/HOL/Computational_Algebra/Primes.thy (diff)
The file was modified src/HOL/Divides.thy (diff)
The file was modified src/HOL/Euclidean_Division.thy (diff)
The file was modified src/HOL/Library/Infinite_Set.thy (diff)
The file was modified src/HOL/Number_Theory/Cong.thy (diff)
The file was modified src/HOL/Number_Theory/Quadratic_Reciprocity.thy (diff)
The file was modified src/HOL/Number_Theory/Residues.thy (diff)
Changeset 66836:4eb431c3f974 by haftmann:
tuned imports
The file was modified src/HOL/Code_Numeral.thy (diff)
The file was modified src/HOL/GCD.thy (diff)
The file was modified src/HOL/HOL.thy (diff)
The file was modified src/HOL/Int.thy (diff)
The file was modified src/HOL/List.thy (diff)
The file was modified src/HOL/Nat_Transfer.thy (diff)
The file was modified src/HOL/Semiring_Normalization.thy (diff)
The file was modified src/HOL/Set_Interval.thy (diff)