Changes

Summary

removed superflous imports of theory Code_Char
proper argument: nb. op is specical token in SML
take warnings about unused parameters more seriously
avoid concrete (anti)mono in theorem names since it could be the other way round

Changeset 8847:2f3bdae911bb by haftmann: removed superflous imports of theory Code_Char
The file was modified	`thys/Algebraic_Numbers/Algebraic_Number_Tests.thy` (diff)
The file was modified	`thys/Linear_Recurrences/Linear_Recurrences_Test.thy` (diff)
The file was modified	`thys/Network_Security_Policy_Verification/Lib/Efficient_Distinct.thy` (diff)
The file was modified	`thys/Network_Security_Policy_Verification/Lib/FiniteListGraph_Impl.thy` (diff)
The file was modified	`thys/Polynomial_Factorization/ROOT` (diff)
The file was modified	`thys/QR_Decomposition/Examples_QR_Abstract_Symbolic.thy` (diff)
The file was modified	`thys/QR_Decomposition/Examples_QR_IArrays_Symbolic.thy` (diff)
The file was modified	`thys/Regex_Equivalence/Regex_Equivalence.thy` (diff)
Changeset 8846:9e3267ecd3b7 by haftmann: proper argument: nb. op is specical token in SML
The file was modified	`thys/FOL_Harrison/FOL_Harrison.thy` (diff)
Changeset 8845:a75c7a23ee1b by haftmann: take warnings about unused parameters more seriously
The file was modified	`thys/FOL_Harrison/FOL_Harrison.thy` (diff)
Changeset 8844:4be24ddf94df by haftmann: avoid concrete (anti)mono in theorem names since it could be the other way round
The file was modified	`thys/Abortable_Linearizable_Modules/Idempotence.thy` (diff)
The file was modified	`thys/Diophantine_Eqns_Lin_Hom/Linear_Diophantine_Equations.thy` (diff)
The file was modified	`thys/Polynomials/Poly_Mapping.thy` (diff)