Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Summary

  1. Avoid \mu and \nu as constant syntax, use LFP and GFP instead.
  2. Revert 5a42eddc11c1.
  3. merged
  4. template for $ISABELLE_HOME_USER/ROOTS;
  5. tuned;
  6. clarified signature: provide all_known information uniformly (it is subject to Sessions.T selection);
  7. reverted 6acb28e5ba41: permissiveness of 1e5ae735e026 should be sufficient;
  8. tuned;
  9. tolerate errors in session structure, although this may lead to confusion about theory imports later on;
  10. clarified errors;
  11. clarified signature; tuned ssh.prefix;
  12. tuned;
  13. Connecting PMFs to infinite sums
  14. Moved material into AFP/Splay_Tree
  15. merged
  16. added PQ with merge
  17. merged
  18. add type of unordered pairs
Changeset 66580:e5b1d4d55bf6 by ballarin:
Avoid \mu and \nu as constant syntax, use LFP and GFP instead.
The file was modified src/HOL/Algebra/Complete_Lattice.thy (diff)
The file was modified src/HOL/Algebra/Lattice.thy (diff)
Changeset 66579:2db3fe23fdaf by ballarin:
Revert 5a42eddc11c1.
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 66578:6a034c6c423f by wenzelm:
merged
Changeset 66577:6e35cf3ce869 by wenzelm:
template for $ISABELLE_HOME_USER/ROOTS;
The file was modified src/Pure/Tools/main.scala (diff)
Changeset 66576:7d4da1c62de7 by wenzelm:
tuned;
The file was modified src/Doc/System/Sessions.thy (diff)
Changeset 66575:191048506504 by wenzelm:
clarified signature: provide all_known information uniformly (it is subject to Sessions.T selection);
The file was modified src/Pure/Thy/sessions.scala (diff)
The file was modified src/Pure/Tools/imports.scala (diff)
Changeset 66574:e16b27bd3f76 by wenzelm:
reverted 6acb28e5ba41: permissiveness of 1e5ae735e026 should be sufficient;
The file was modified NEWS (diff)
The file was modified src/Doc/JEdit/JEdit.thy (diff)
The file was modified src/Tools/jEdit/lib/Tools/jedit (diff)
The file was modified src/Tools/jEdit/src/jedit_sessions.scala (diff)
Changeset 66573:a6401a6417cf by wenzelm:
tuned;
The file was modified src/Pure/Thy/sessions.scala (diff)
Changeset 66572:1e5ae735e026 by wenzelm:
tolerate errors in session structure, although this may lead to confusion about theory imports later on;
The file was modified src/Tools/jEdit/src/jedit_resources.scala (diff)
The file was modified src/Tools/jEdit/src/jedit_sessions.scala (diff)
The file was modified src/Tools/jEdit/src/plugin.scala (diff)
Changeset 66571:0fdeb24e535e by wenzelm:
clarified errors;
The file was modified src/Pure/Thy/sessions.scala (diff)
The file was modified src/Pure/Tools/build.scala (diff)
The file was modified src/Pure/Tools/imports.scala (diff)
Changeset 66570:9af879e222cc by wenzelm:
clarified signature;<br>tuned ssh.prefix;
The file was modified src/Pure/Admin/build_history.scala (diff)
The file was modified src/Pure/General/mercurial.scala (diff)
The file was modified src/Pure/General/ssh.scala (diff)
Changeset 66569:1a475e59c70f by wenzelm:
tuned;
The file was modified src/Pure/General/mercurial.scala (diff)
Changeset 66568:52b5cf533fd6 by eberlm _eberlm@in.tum.de_:
Connecting PMFs to infinite sums
The file was modified src/HOL/Analysis/Infinite_Set_Sum.thy (diff)
The file was modified src/HOL/Probability/Probability_Mass_Function.thy (diff)
Changeset 66567:dd47c9843598 by nipkow:
Moved material into AFP/Splay_Tree
The file was modified src/HOL/ROOT (diff)
The file was removedsrc/HOL/Data_Structures/Splay_Map.thy
The file was removedsrc/HOL/Data_Structures/Splay_Set.thy
Changeset 66566:a14bbbaa628d by nipkow:
merged
Changeset 66565:ff561d9cb661 by nipkow:
added PQ with merge
The file was modified src/HOL/Data_Structures/Binomial_Heap.thy (diff)
The file was modified src/HOL/Data_Structures/Leftist_Heap.thy (diff)
The file was modified src/HOL/Data_Structures/Priority_Queue.thy (diff)
Changeset 66564:090c4474f310 by Andreas Lochbihler:
merged
Changeset 66563:87b9eb69d5ba by Andreas Lochbihler:
add type of unordered pairs
The file was addedsrc/HOL/Library/Uprod.thy
The file was modified CONTRIBUTORS (diff)
The file was modified NEWS (diff)
The file was modified src/HOL/Library/Library.thy (diff)