Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Summary

  1. back to more liberal imports (amending 908a27a4b9c9): tolerate mixed situations like "GCD" vs. "~~/src/HOL/GCD";
  2. tuned headers;
  3. proper imports; tuned headers;
Changeset 65368:7fb5aad28f38 by wenzelm:
back to more liberal imports (amending 908a27a4b9c9): tolerate mixed situations like "GCD" vs. "~~/src/HOL/GCD";
The file was modified src/Pure/PIDE/resources.scala (diff)
Changeset 65367:83c30e290702 by wenzelm:
tuned headers;
The file was modified src/HOL/Library/Cancellation/cancel.ML (diff)
The file was modified src/HOL/Library/Cancellation/cancel_data.ML (diff)
The file was modified src/HOL/Library/Cancellation/cancel_simprocs.ML (diff)
The file was modified src/Pure/Tools/spell_checker.scala (diff)
The file was modified src/Tools/VSCode/src/build_vscode.scala (diff)
Changeset 65366:10ca63a18e56 by wenzelm:
proper imports;<br>tuned headers;
The file was modified src/HOL/Library/Combine_PER.thy (diff)
The file was modified src/HOL/Library/Complete_Partial_Order2.thy (diff)
The file was modified src/HOL/Library/Extended.thy (diff)
The file was modified src/HOL/Library/Multiset_Permutations.thy (diff)
The file was modified src/HOL/Library/Normalized_Fraction.thy (diff)
The file was modified src/HOL/Library/Polynomial.thy (diff)
The file was modified src/HOL/Library/Polynomial_FPS.thy (diff)
The file was modified src/HOL/Library/Polynomial_Factorial.thy (diff)
The file was modified src/HOL/Library/Stream.thy (diff)