Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Changes from Mercurial (hg https://bitbucket.org/isa-afp/afp-devel/ default)

Summary

  1. merged
  2. adjusted to devel
Changeset 10611:e783400723b7 by nipkow:
merged
Changeset 10610:0291608f6cee by nipkow:
adjusted to devel
The file was modified thys/Root_Balanced_Tree/Root_Balanced_Tree.thy

Changes from Mercurial (hg http://isabelle.in.tum.de/repos/isabelle/ default)

Summary

  1. merged
  2. Enforced precodition "n <= length xs" to avoid relying on "hd []".
  3. Generalisation of many theorems to a more abstract type class (suggested by Mr Anonymous)
  4. tuned
  5. added lemma
Changeset 70748:b3b84b71e398 by nipkow:
merged
Changeset 70747:548420d389ea by nipkow:
Enforced precodition &quot;n &lt;= length xs&quot; to avoid relying on &quot;hd []&quot;.
The file was modified src/HOL/Data_Structures/Balance.thy
Changeset 70746:cf7b5020c207 by paulson _lp15@cam.ac.uk_:
Generalisation of many theorems to a more abstract type class (suggested by Mr Anonymous)
The file was modified src/HOL/Set_Interval.thy
Changeset 70745:be8e617b6eb3 by nipkow:
tuned
The file was modified src/HOL/Data_Structures/Tree2.thy
Changeset 70744:b605c9cf82a2 by nipkow:
added lemma
The file was modified src/HOL/Data_Structures/Tree2.thy