Skip to content
[Jenkins]Jenkins
log in
Success

Changes

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

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
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
The file was modified src/HOL/Library/NList.thy
Changeset 75803:40e16228405e by nipkow:
new lemma
The file was modified NEWS
The file was modified src/HOL/Library/NList.thy
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

Changes from Mercurial (hg https://foss.heptapod.net/isa-afp/afp-devel/ default)

Summary

  1. adapted to NLists.thy
  2. merged
  3. use Library/NList.thy now
Changeset 12910:56d5a40ba8fc by nipkow:
adapted to NLists.thy
The file was modified thys/Dominance_CHK/Dom_Kildall_Property.thy
The file was modified thys/HRB-Slicing/JinjaVM_Inter/JVMCFG.thy
The file was modified thys/Slicing/JinjaVM/JVMCFG.thy
Changeset 12909:64e1c7e89ad3 by nipkow:
merged
Changeset 12908:965b1fce10d0 by nipkow:
use Library/NList.thy now
The file was modified thys/Jinja/BV/BVExec.thy
The file was modified thys/Jinja/BV/JVM_SemiType.thy
The file was modified thys/Jinja/BV/LBVJVM.thy
The file was modified thys/Jinja/BV/TF_JVM.thy
The file was modified thys/Jinja/Compiler/TypeComp.thy
The file was modified thys/Jinja/DFA/Kildall_1.thy
The file was modified thys/Jinja/DFA/Kildall_2.thy
The file was modified thys/Jinja/DFA/LBVCorrect.thy
The file was modified thys/Jinja/DFA/Listn.thy
The file was modified thys/Jinja/DFA/Typing_Framework_2.thy
The file was modified thys/JinjaDCI/BV/BVExec.thy
The file was modified thys/JinjaDCI/BV/ClassAdd.thy
The file was modified thys/JinjaDCI/BV/JVM_SemiType.thy
The file was modified thys/JinjaDCI/BV/LBVJVM.thy
The file was modified thys/JinjaDCI/BV/TF_JVM.thy
The file was modified thys/JinjaDCI/Compiler/TypeComp.thy