Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Summary

  1. clarified file names;
  2. clarified build_polyml_component: include IDE entry point for ML compiler;
  3. merged
  4. tuned spelling;
  5. new examples of BNF lifting across quotients using a new theory of confluence, which simplifies the relator subdistributivity proof obligation (a few new useful notions were added to HOL; notably the symmetric and equivalence closures of a relation)
Changeset 71397:028edb1e5b99 by wenzelm:
clarified file names;
The file was modified Admin/polyml/settings (diff)
The file was modified src/Pure/Tools/doc.scala (diff)
Changeset 71396:c1c61d0d8e7c by wenzelm:
clarified build_polyml_component: include IDE entry point for ML compiler;
The file was modified Admin/polyml/settings (diff)
The file was modified src/Pure/Admin/build_polyml.scala (diff)
Changeset 71395:d7f8ee80ad42 by wenzelm:
merged
Changeset 71394:933ad2385480 by wenzelm:
tuned spelling;
The file was modified src/HOL/Tools/Quickcheck/exhaustive_generators.ML (diff)
Changeset 71393:fce780f9c9c6 by traytel:
new examples of BNF lifting across quotients using a new theory of confluence,<br>which simplifies the relator subdistributivity proof obligation<br>(a few new useful notions were added to HOL;<br>notably the symmetric and equivalence closures of a relation)
The file was addedsrc/HOL/Datatype_Examples/Cyclic_List.thy
The file was addedsrc/HOL/Datatype_Examples/Dlist.thy
The file was addedsrc/HOL/Datatype_Examples/Free_Idempotent_Monoid.thy
The file was addedsrc/HOL/Datatype_Examples/LDL.thy
The file was addedsrc/HOL/Library/Confluence.thy
The file was addedsrc/HOL/Library/Confluent_Quotient.thy
The file was modified src/Doc/Datatypes/Datatypes.thy (diff)
The file was modified src/HOL/Equiv_Relations.thy (diff)
The file was modified src/HOL/Library/Library.thy (diff)
The file was modified src/HOL/List.thy (diff)
The file was modified src/HOL/Quotient.thy (diff)
The file was modified src/HOL/ROOT (diff)
The file was modified src/HOL/Tools/BNF/bnf_lift.ML (diff)
The file was modified src/HOL/Transitive_Closure.thy (diff)