Changes from Mercurial (hg https://bitbucket.org/isa-afp/afp-devel/ default)
Summary
- added DBA binary union operation
- removed unnecessary type annotation
- added cardinality theorems for automata constructions
The file was modified | thys/Transition_Systems_and_Automata/Automata/DBA_Combine.thy |
The file was modified | thys/Buchi_Complementation/Complementation_Final.thy |
The file was modified | thys/Transition_Systems_and_Automata/Automata/DBA_Combine.thy |
The file was modified | thys/Transition_Systems_and_Automata/Automata/DCA_Combine.thy |
The file was modified | thys/Transition_Systems_and_Automata/Automata/DGBA.thy |
The file was modified | thys/Transition_Systems_and_Automata/Automata/DGCA.thy |
The file was modified | thys/Transition_Systems_and_Automata/Automata/DRA_Combine.thy |
The file was modified | thys/Transition_Systems_and_Automata/Basic/Basic.thy |
The file was modified | thys/Transition_Systems_and_Automata/Basic/Sequence.thy |
The file was modified | thys/Transition_Systems_and_Automata/Transition_Systems/Transition_System_Degeneralization.thy |
Changes from Mercurial (hg http://isabelle.in.tum.de/repos/isabelle/ default)
Summary
- added DBA binary union operation
- removed unnecessary type annotation
- added cardinality theorems for automata constructions
The file was modified | thys/Transition_Systems_and_Automata/Automata/DBA_Combine.thy |
The file was modified | thys/Buchi_Complementation/Complementation_Final.thy |
The file was modified | thys/Transition_Systems_and_Automata/Automata/DBA_Combine.thy |
The file was modified | thys/Transition_Systems_and_Automata/Automata/DCA_Combine.thy |
The file was modified | thys/Transition_Systems_and_Automata/Automata/DGBA.thy |
The file was modified | thys/Transition_Systems_and_Automata/Automata/DGCA.thy |
The file was modified | thys/Transition_Systems_and_Automata/Automata/DRA_Combine.thy |
The file was modified | thys/Transition_Systems_and_Automata/Basic/Basic.thy |
The file was modified | thys/Transition_Systems_and_Automata/Basic/Sequence.thy |
The file was modified | thys/Transition_Systems_and_Automata/Transition_Systems/Transition_System_Degeneralization.thy |