Changes

Summary

MFMC_Countable: ported from ereal to ennreal
separate target in ROOT-file: Algebraic_Number_Lib (does not include expensive Algebraic_Number_Tests)
tuned;
repaired proof;
merge
removing legacy vString, using string directly now

Changeset 6742:83c0fef83e3f by hoelzl: MFMC_Countable: ported from ereal to ennreal
The file was modified	`thys/MFMC_Countable/MFMC_Misc.thy` (diff)
The file was modified	`thys/MFMC_Countable/Max_Flow_Min_Cut_Countable.thy` (diff)
The file was modified	`thys/MFMC_Countable/Rel_PMF_Characterisation.thy` (diff)
Changeset 6741:9079cfb3406b by rene thiemann _rene.thiemann@uibk.ac.at_: separate target in ROOT-file: Algebraic_Number_Lib<br>(does not include expensive Algebraic_Number_Tests)
The file was modified	`thys/Algebraic_Numbers/ROOT` (diff)
Changeset 6740:2580d612c514 by wenzelm: tuned;
The file was modified	`thys/Featherweight_OCL/UML_Types.thy` (diff)
The file was modified	`thys/Isabelle_Meta_Model/toy_example/embedding/Generator_dynamic.thy` (diff)
Changeset 6739:b8649d48fed5 by wenzelm: repaired proof;
The file was modified	`thys/Tree_Decomposition/TreeDecomposition.thy` (diff)
Changeset 6738:8f70b594c97c by cornelius diekmann _diekmann@net.in.tum.de_: merge
Changeset 6737:a362c0c70a5c by cornelius diekmann _diekmann@net.in.tum.de_: removing legacy vString, using string directly now
The file was modified	`thys/Network_Security_Policy_Verification/Example_BLP.thy` (diff)
The file was modified	`thys/Network_Security_Policy_Verification/Examples/Distributed_WebApp.thy` (diff)
The file was modified	`thys/Network_Security_Policy_Verification/Examples/Example_Forte14.thy` (diff)
The file was modified	`thys/Network_Security_Policy_Verification/Examples/Impl_List_Playground.thy` (diff)
The file was modified	`thys/Network_Security_Policy_Verification/Examples/Impl_List_Playground_ChairNetwork.thy` (diff)
The file was modified	`thys/Network_Security_Policy_Verification/Examples/Impl_List_Playground_ChairNetwork_statefulpolicy_example.thy` (diff)
The file was modified	`thys/Network_Security_Policy_Verification/Security_Invariants/SINVAR_BLPbasic_impl.thy` (diff)
The file was modified	`thys/Network_Security_Policy_Verification/Security_Invariants/SINVAR_DomainHierarchyNG_impl.thy` (diff)
The file was modified	`thys/Network_Security_Policy_Verification/TopoS_Impl.thy` (diff)
The file was modified	`thys/Network_Security_Policy_Verification/TopoS_Interface.thy` (diff)
The file was modified	`thys/Network_Security_Policy_Verification/TopoS_Vertices.thy` (diff)