Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Summary

  1. generalized confluence-based subdistributivity theorem for quotients; new example that triggered the generalization
  2. Backed out changeset 3fdb94d87e0e
  3. Backed out changeset b867b436f372
Changeset 73398:180981b87929 by traytel:
generalized confluence-based subdistributivity theorem for quotients;<br>new example that triggered the generalization
The file was addedsrc/HOL/Datatype_Examples/Regex_ACI.thy
The file was addedsrc/HOL/Datatype_Examples/Regex_ACIDZ.thy
The file was modified src/HOL/Datatype_Examples/Cyclic_List.thy (diff)
The file was modified src/HOL/Datatype_Examples/Free_Idempotent_Monoid.thy (diff)
The file was modified src/HOL/Library/Confluent_Quotient.thy (diff)
The file was modified src/HOL/Library/Dlist.thy (diff)
The file was modified src/HOL/ROOT (diff)
The file was removedsrc/HOL/Datatype_Examples/LDL.thy
Changeset 73397:d47c8a89c6a5 by desharna:
Backed out changeset 3fdb94d87e0e
The file was modified src/HOL/Library/Sublist.thy (diff)
Changeset 73396:8a1c6c7909c9 by desharna:
Backed out changeset b867b436f372
The file was modified src/HOL/List.thy (diff)