# ChangeLog
All notable changes to this project will be documented in this file.

## [1.4.0] - 2021-05-14

### Added
* CoW/CoWBasic: 
** locale two_morphisms
** section on reversed morphism and composition
** code equations for left quotient
** several other lemmas
* CoW_Lyndon/Lyndon:
** code equations for Lyndon
** lemma Lyndon_mono_smallest
* introductory texts

### Changed
* changed directory names to match session names (Basics->CoW, Lyndon->CoW_Lyndon, Graph_Lemma->CoW_Graph_Lemma)
* contains of CoW/Borders moved to CoW/CoWBasic
* many optimizations


## [1.3.0] - 2021-04-13

### Added
* Reversal_Symmetry theory and application of the reversed attribute throughout all theories
* Basics/Submonoids: added Binary Code
* Basics/CoWBasic: some auxiliary lemmas added

### Changed
* new directory structure ready for AFP sessions (main theory files were moved to directoires Basics, Graph_Lemma, Lyndon, or Equations)
* Borders split into Borders and Lyndon
* Borders_Addition renamed to Lyndon_Addition
* imports respect planned session structure
* many proofs were optimized

### Removed
* Basics/CoWBasic: non-empty element abbreviation was deleted


## [1.2.0] - 2021-02-22

### Added
* Overlaps
* examples/ExampleBasic
* CoWBasic: few elementary lemmas

### Changed
* compatible with Isabelle 2021
* factor interpretation moved from Submonoids to Overlaps
* CoWBasic: various optimizations
* PeriodicityLemma: proof optimizations
 
## [1.1.0] - 2021-02-01
  
### Added

* theorem Lyndon_Schutzenberger (in LyndonSchutzenberger.thy)
* theorem free_hull_inter (in Submonoids.thy)
 
### Changed

* better integration with Sublist.thy (in CoWBasic.thy)
* naming optimization (in CoWBasic.thy)
* few additions concering conjugation and primitivity (in CoWBasic.thy)
* proof optimizations
 
## [1.0.0] - 2021-01-17

Initial initial version covering essential, graph lemma, periodicity lemma, LS teorem, Lyndon words.