Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Summary

  1. - added locale dynamic_architectures - added proposition to assert correctness of evaluation mapping - added definitions and introduction/elimination rules for basic operators: basic predicates, true and false, conjunction, disjunction, implication, quantifications - added definition for weak until - behavior trace assertions are modified to predicate transformers
Changeset 8185:471fae0c8776 by diego marmsoler _diego.marmsoler@tum.de_:
- added locale dynamic_architectures<br>- added proposition to assert correctness of evaluation mapping<br>- added definitions and introduction/elimination rules for basic operators: basic predicates, true and false, conjunction, disjunction, implication, quantifications<br>- added definition for weak until<br>- behavior trace assertions are modified to predicate transformers
The file was modified thys/DynamicArchitectures/Configuration_Traces.thy (diff)
The file was modified thys/DynamicArchitectures/Dynamic_Architecture_Calculus.thy (diff)
The file was modified thys/DynamicArchitectures/document/root.tex (diff)