Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Summary

  1. tuned proof
  2. simplified defns
  3. "undefined" not needed, [] is perfectly natural
  4. tuned
Changeset 68972:96b15934a17a by nipkow:
tuned proof
The file was modified src/HOL/Data_Structures/Sorting.thy (diff)
Changeset 68971:938f4058c07c by nipkow:
simplified defns
The file was modified src/HOL/Data_Structures/Sorting.thy (diff)
Changeset 68970:b0dfe57dfa09 by nipkow:
"undefined" not needed, [] is perfectly natural
The file was modified src/HOL/Data_Structures/Sorting.thy (diff)
Changeset 68969:7a9118e63cad by nipkow:
tuned
The file was modified src/HOL/Data_Structures/Set2_Join.thy (diff)