Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Summary

  1. merged
  2. tuned signature;
  3. added spaces because otherwise nonatomic arguments look awful: BIGf x -> BIG f x
  4. merged
  5. merged
  6. tiny cleanup
  7. merged
  8. A few new results, elimination of duplicates and more use of "pairwise"
  9. tuned
  10. tuned "=" syntax declarations; made "~=" uniformly "infix"
Changeset 68982:807099160468 by wenzelm:
merged
Changeset 68981:30daac7848b9 by wenzelm:
tuned signature;
The file was modified src/Pure/Thy/thy_resources.scala (diff)
The file was modified src/Pure/Tools/dump.scala (diff)
Changeset 68980:5717fbc55521 by nipkow:
added spaces because otherwise nonatomic arguments look awful: BIGf x -> BIG f x
The file was modified src/HOL/Complete_Lattices.thy (diff)
The file was modified src/HOL/Lattices_Big.thy (diff)
The file was modified src/HOL/Library/Complete_Partial_Order2.thy (diff)
The file was modified src/HOL/Library/Lattice_Syntax.thy (diff)
The file was modified src/HOL/Library/Multiset.thy (diff)
The file was modified src/HOL/Library/Option_ord.thy (diff)
The file was modified src/HOL/Main.thy (diff)
Changeset 68979:e2244e5707dd by paulson:
merged
Changeset 68978:26be7c0d65a1 by paulson:
merged
Changeset 68977:c73ca43087c0 by paulson _lp15@cam.ac.uk_:
tiny cleanup
The file was modified src/HOL/Library/Omega_Words_Fun.thy (diff)
Changeset 68976:105bbce656a5 by paulson:
merged
Changeset 68975:5ce4d117cea7 by paulson _lp15@cam.ac.uk_:
A few new results, elimination of duplicates and more use of "pairwise"
The file was modified src/HOL/Algebra/AbelCoset.thy (diff)
The file was modified src/HOL/Algebra/Chinese_Remainder.thy (diff)
The file was modified src/HOL/Algebra/Coset.thy (diff)
The file was modified src/HOL/Algebra/Group_Action.thy (diff)
The file was modified src/HOL/Algebra/Sym_Groups.thy (diff)
The file was modified src/HOL/Computational_Algebra/Formal_Power_Series.thy (diff)
The file was modified src/HOL/Finite_Set.thy (diff)
The file was modified src/HOL/Groups_Big.thy (diff)
The file was modified src/HOL/HOL.thy (diff)
The file was modified src/HOL/Hilbert_Choice.thy (diff)
The file was modified src/HOL/Hoare_Parallel/RG_Hoare.thy (diff)
The file was modified src/HOL/Library/Stirling.thy (diff)
The file was modified src/HOL/List.thy (diff)
The file was modified src/HOL/Probability/ex/Dining_Cryptographers.thy (diff)
The file was modified src/HOL/Zorn.thy (diff)
Changeset 68974:271026e97ca2 by nipkow:
tuned
The file was modified src/HOL/Data_Structures/Sorting.thy (diff)
Changeset 68973:a1e26440efb8 by nipkow:
tuned "=" syntax declarations; made "~=" uniformly "infix"
The file was modified src/HOL/HOL.thy (diff)