Skip to content
Success

Changes

Summary

  1. merged
  2. exclude file name components that are special on Windows;
  3. reject further illegal chars according to https://docs.microsoft.com/en-us/windows/desktop/fileio/naming-a-file
  4. tuned;
  5. more strict check: avoid confusion of Path.basic with Path.current / Path.parent;
  6. tuned;
  7. prefer naming convention from datatype package for strong congruence rules
  8. redundant
Changeset 69552:b85f4c5cb588 by wenzelm:
merged
Changeset 69551:adb52af5ba55 by wenzelm:
exclude file name components that are special on Windows;
The file was modified src/Doc/Isar_Ref/Outer_Syntax.thy (diff)
The file was modified src/Pure/General/path.scala (diff)
The file was modified src/Pure/Isar/token.scala (diff)
Changeset 69550:57ff523d9008 by wenzelm:
reject further illegal chars according to https://docs.microsoft.com/en-us/windows/desktop/fileio/naming-a-file
The file was modified src/Pure/General/path.ML (diff)
The file was modified src/Pure/General/path.scala (diff)
Changeset 69549:612a02019f48 by wenzelm:
tuned;
The file was modified src/Pure/General/path.ML (diff)
The file was modified src/Pure/General/path.scala (diff)
Changeset 69548:415dc92050a6 by wenzelm:
more strict check: avoid confusion of Path.basic with Path.current / Path.parent;
The file was modified src/Pure/General/path.ML (diff)
The file was modified src/Pure/General/path.scala (diff)
Changeset 69547:47c589d3af77 by wenzelm:
tuned;
The file was modified src/Pure/General/path.ML (diff)
The file was modified src/Pure/General/path.scala (diff)
Changeset 69546:27dae626822b by haftmann:
prefer naming convention from datatype package for strong congruence rules
The file was modified NEWS (diff)
The file was modified src/HOL/Analysis/Bochner_Integration.thy (diff)
The file was modified src/HOL/Analysis/Caratheodory.thy (diff)
The file was modified src/HOL/Analysis/L2_Norm.thy (diff)
The file was modified src/HOL/Analysis/Lebesgue_Measure.thy (diff)
The file was modified src/HOL/Analysis/Measure_Space.thy (diff)
The file was modified src/HOL/Analysis/Nonnegative_Lebesgue_Integration.thy (diff)
The file was modified src/HOL/Analysis/Sigma_Algebra.thy (diff)
The file was modified src/HOL/Complete_Lattices.thy (diff)
The file was modified src/HOL/Data_Structures/Braun_Tree.thy (diff)
The file was modified src/HOL/Hoare_Parallel/RG_Examples.thy (diff)
The file was modified src/HOL/Library/Complete_Partial_Order2.thy (diff)
The file was modified src/HOL/Probability/Giry_Monad.thy (diff)
The file was modified src/HOL/Set.thy (diff)
The file was modified src/HOL/Topological_Spaces.thy (diff)
Changeset 69545:4aed40ecfb43 by haftmann:
redundant
The file was modified src/HOL/ROOT (diff)