Changes

Changes from Mercurial (hg https://bitbucket.org/isa-afp/afp-devel/ default)

Summary

Implement equivalence relation with unfolding for LTL Master Theorem
Proof of Restricted Master Theorem on LTL

Changeset 10609:a2c03373dc20 by benedikt seidl _benedikt.seidl@tum.de_: Implement equivalence relation with unfolding for LTL Master Theorem
The file was added	`thys/LTL_Master_Theorem/Logical_Characterization/Extra_Equivalence_Relations.thy`
The file was modified	`thys/LTL_Master_Theorem/Code_Export.thy`
The file was modified	`thys/LTL_Master_Theorem/LTL_to_DRA/DRA_Construction.thy`
The file was modified	`thys/LTL_Master_Theorem/LTL_to_DRA/DRA_Implementation.thy`
The file was modified	`thys/LTL_Master_Theorem/LTL_to_DRA/DRA_Instantiation.thy`
The file was modified	`thys/LTL_Master_Theorem/LTL_to_DRA/Transition_Functions.thy`
The file was modified	`thys/LTL_Master_Theorem/Logical_Characterization/Advice.thy`
The file was modified	`thys/LTL_Master_Theorem/code/ltl_to_dra_cli.sml`
Changeset 10608:db7040379c22 by benedikt seidl _benedikt.seidl@tum.de_: Proof of Restricted Master Theorem on LTL
The file was added	`thys/LTL_Master_Theorem/Logical_Characterization/Restricted_Master_Theorem.thy`
The file was modified	`thys/LTL/Equivalence_Relations.thy`
The file was modified	`thys/LTL/LTL.thy`
The file was modified	`thys/LTL_Master_Theorem/Logical_Characterization/Advice.thy`
The file was modified	`thys/LTL_Master_Theorem/Logical_Characterization/After.thy`
The file was modified	`thys/LTL_Master_Theorem/Logical_Characterization/Master_Theorem.thy`
The file was modified	`thys/LTL_Master_Theorem/Logical_Characterization/Syntactic_Fragments_and_Stability.thy`
The file was modified	`thys/LTL_Master_Theorem/ROOT`