Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Summary

  1. removing the [simp] attribute breaks too many AFP entries severely
  2. nlists is picked up automatically but conflicts with the RBT setup
  3. new lemma
  4. merged
  5. New theory of fixed length lists
Changeset 75805:3581dcee70db by nipkow:
removing the [simp] attribute breaks too many AFP entries severely
The file was modified src/HOL/Library/NList.thy (diff)
Changeset 75804:dd04e81172a8 by nipkow:
nlists is picked up automatically but conflicts with the RBT setup
The file was modified src/HOL/Codegenerator_Test/Generate_Efficient_Datastructures.thy (diff)
The file was modified src/HOL/Library/NList.thy (diff)
Changeset 75803:40e16228405e by nipkow:
new lemma
The file was modified NEWS (diff)
The file was modified src/HOL/Library/NList.thy (diff)
Changeset 75802:2a049b402e53 by nipkow:
merged
Changeset 75801:5c1856aaf03d by nipkow:
New theory of fixed length lists
The file was addedsrc/HOL/Library/NList.thy
The file was modified src/HOL/Library/Library.thy (diff)