Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Summary

  1. merged
  2. Fixes for Sup{} = (0::nat)
  3. abbrevs for the Uniq quantifier; trying Sup_nat_def to allow zero (experimentally)
  4. clarified session imports: avoid bulky HOL-Library image;
  5. tuned -- avoid warning;
  6. "app" -> "join" for RBTs
  7. "app" -> "join" for uniformity with Join theory; tuned defs
Changeset 71835:455b010d8436 by paulson:
merged
Changeset 71834:919a55257e62 by paulson _lp15@cam.ac.uk_:
Fixes for Sup{} = (0::nat)
The file was modified NEWS (diff)
The file was modified src/HOL/Analysis/Measurable.thy (diff)
The file was modified src/HOL/Conditionally_Complete_Lattices.thy (diff)
The file was modified src/HOL/Library/Extended_Nonnegative_Real.thy (diff)
Changeset 71833:ff6f3b09b8b4 by paulson _lp15@cam.ac.uk_:
abbrevs for the Uniq quantifier; trying Sup_nat_def to allow zero (experimentally)
The file was modified src/HOL/Conditionally_Complete_Lattices.thy (diff)
The file was modified src/HOL/HOL.thy (diff)
Changeset 71832:f61b19358a8f by wenzelm:
clarified session imports: avoid bulky HOL-Library image;
The file was modified src/HOL/ROOT (diff)
Changeset 71831:26c4af1e4ffe by wenzelm:
tuned -- avoid warning;
The file was modified src/HOL/Isar_Examples/Higher_Order_Logic.thy (diff)
Changeset 71830:7a997ead54b0 by nipkow:
"app" -> "join" for RBTs
The file was modified src/HOL/Data_Structures/RBT.thy (diff)
The file was modified src/HOL/Data_Structures/RBT_Map.thy (diff)
The file was modified src/HOL/Data_Structures/RBT_Set.thy (diff)
The file was modified src/HOL/Data_Structures/RBT_Set2.thy (diff)
Changeset 71829:6f2663df8374 by nipkow:
"app" -> "join" for uniformity with Join theory; tuned defs
The file was modified src/HOL/Data_Structures/Set_Specs.thy (diff)
The file was modified src/HOL/Data_Structures/Tree_Set.thy (diff)