Skip to content
Success

Changes

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

Summary

  1. added DBA binary union operation
  2. removed unnecessary type annotation
  3. added cardinality theorems for automata constructions
Changeset 10025:f522bb424673 by julian brunner _julianbrunner@gmail.com_:
added DBA binary union operation
The file was modified thys/Transition_Systems_and_Automata/Automata/DBA_Combine.thy
Changeset 10024:518de673b263 by julian brunner _julianbrunner@gmail.com_:
removed unnecessary type annotation
The file was modified thys/Buchi_Complementation/Complementation_Final.thy
Changeset 10023:c27157a8fb27 by julian brunner _julianbrunner@gmail.com_:
added cardinality theorems for automata constructions
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

  1. added DBA binary union operation
  2. removed unnecessary type annotation
  3. added cardinality theorems for automata constructions
Changeset 10025:f522bb424673 by julian brunner _julianbrunner@gmail.com_:
added DBA binary union operation
The file was modified thys/Transition_Systems_and_Automata/Automata/DBA_Combine.thy
Changeset 10024:518de673b263 by julian brunner _julianbrunner@gmail.com_:
removed unnecessary type annotation
The file was modified thys/Buchi_Complementation/Complementation_Final.thy
Changeset 10023:c27157a8fb27 by julian brunner _julianbrunner@gmail.com_:
added cardinality theorems for automata constructions
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