Summary
- removed dependence of Graph-Theory from Perron-Frobenius
- tightened bound of paths by 1
- removed unused theorems cmod_plus_eqD, ...
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) |
The file was modified | thys/Graph_Theory/Arc_Walk.thy (diff) |
The file was modified | thys/Perron_Frobenius/Perron_Frobenius_Aux_2.thy (diff) |