Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Summary

  1. swapping of theory dependency yields less pervasive syntax requiring popular symbols \<mu>, \<nu>
  2. more correct output syntax declaration
  3. tuned
  4. Merge (non-trivial)
  5. More tidying, and renaming of theorems
  6. merged
  7. More tidying up of monotone_convergence_interval
  8. tuning (proofs and code)
  9. upgraded CVC4 component to fix abnormal termination reported by Larry Paulson
  10. dedicated local for "operative" avoids namespace pollution
Changeset 66501:5a42eddc11c1 by haftmann:
swapping of theory dependency yields less pervasive syntax requiring popular symbols \&lt;mu&gt;, \&lt;nu&gt;
The file was modified src/HOL/Algebra/Complete_Lattice.thy (diff)
The file was modified src/HOL/Algebra/Divisibility.thy (diff)
The file was modified src/HOL/Algebra/Group.thy (diff)
Changeset 66500:ba94aeb02fbc by haftmann:
more correct output syntax declaration
The file was modified src/HOL/Algebra/Multiplicative_Group.thy (diff)
Changeset 66499:8367a4f25781 by nipkow:
tuned
The file was modified src/HOL/Data_Structures/Base_FDS.thy (diff)
The file was modified src/HOL/Data_Structures/Leftist_Heap.thy (diff)
Changeset 66498:97fc319d6089 by paulson _lp15@cam.ac.uk_:
Merge (non-trivial)
Changeset 66497:18a6478a574c by paulson _lp15@cam.ac.uk_:
More tidying, and renaming of theorems
The file was modified src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy (diff)
The file was modified src/HOL/Analysis/Henstock_Kurzweil_Integration.thy (diff)
The file was modified src/HOL/Analysis/Improper_Integral.thy (diff)
The file was modified src/HOL/Analysis/Tagged_Division.thy (diff)
Changeset 66496:001d4a9986a2 by paulson:
merged
Changeset 66495:0b46bd081228 by paulson _lp15@cam.ac.uk_:
More tidying up of monotone_convergence_interval
The file was modified src/HOL/Analysis/Harmonic_Numbers.thy (diff)
The file was modified src/HOL/Analysis/Henstock_Kurzweil_Integration.thy (diff)
Changeset 66494:8645dc296dca by blanchet:
tuning (proofs and code)
The file was modified src/HOL/Library/Multiset.thy (diff)
The file was modified src/HOL/Tools/BNF/bnf_lfp_size.ML (diff)
Changeset 66493:c94c55cc8d86 by blanchet:
upgraded CVC4 component to fix abnormal termination reported by Larry Paulson
The file was modified Admin/components/components.sha1 (diff)
The file was modified Admin/components/main (diff)
Changeset 66492:d7206afe2d28 by haftmann:
dedicated local for &quot;operative&quot; avoids namespace pollution
The file was modified src/HOL/Analysis/Henstock_Kurzweil_Integration.thy (diff)
The file was modified src/HOL/Analysis/Tagged_Division.thy (diff)