Skip to content
Success

Changes

Summary

  1. removed dependence of Graph-Theory from Perron-Frobenius
  2. tightened bound of paths by 1
  3. removed unused theorems cmod_plus_eqD, ...
Changeset 8450:bda1f1ce8a1c by rene thiemann _rene.thiemann@uibk.ac.at_:
removed dependence of Graph-Theory from Perron-Frobenius
The file was modified thys/Perron_Frobenius/Perron_Frobenius_Aux_2.thy (diff)
The file was modified thys/Perron_Frobenius/Perron_Frobenius_General.thy (diff)
The file was modified thys/Perron_Frobenius/Perron_Frobenius_Irreducible.thy (diff)
The file was modified thys/Perron_Frobenius/ROOT (diff)
Changeset 8449:7e3e379e5a7f by rene thiemann _rene.thiemann@uibk.ac.at_:
tightened bound of paths by 1
The file was modified thys/Graph_Theory/Arc_Walk.thy (diff)
Changeset 8448:2cc148b6f475 by rene thiemann _rene.thiemann@uibk.ac.at_:
removed unused theorems cmod_plus_eqD, ...
The file was modified thys/Perron_Frobenius/Perron_Frobenius_Aux_2.thy (diff)