This is just a hint as a spin-off from the reform of session-qualified
theory names.
The "isabelle imports" tool is able to detect unused theory sources --
that is important to check the sanity of the overall theory graph, e.g.
wrongly qualified names can lead to files that are no longer used.
Here is the result for AFP (Isabelle/158c513a39f5 and AFP/0a57dd7e945a),
using the following command-line:
isabelle imports -M -d '~~/src/Benchmarks' -d '$AFP' -a
unused file
"/home/makarius/isabelle/repos/AFP/thys/Berlekamp_Zassenhaus/Tests.thy"
unused file
"/home/makarius/isabelle/repos/AFP/thys/Consensus_Refined/MRU/Two_Step_MRU.thy"
unused file
"/home/makarius/isabelle/repos/AFP/thys/Flyspeck-Tame/ArchStat.thy"
unused file
"/home/makarius/isabelle/repos/AFP/thys/Isabelle_Meta_Model/toy_example/document_generated/Design_generated.thy"
unused file
"/home/makarius/isabelle/repos/AFP/thys/Key_Agreement_Strong_Adversaries/Import_all.thy"
unused file
"/home/makarius/isabelle/repos/AFP/thys/Pi_Calculus/Late_Hennessy.thy"
unused file
"/home/makarius/isabelle/repos/AFP/thys/Pi_Calculus/Late_Hennessy_Subst.thy"
unused file
"/home/makarius/isabelle/repos/AFP/thys/Pi_Calculus/Res_Pres.thy"
unused file
"/home/makarius/isabelle/repos/AFP/thys/Pi_Calculus/Strong_Early_Bisim_Subst_SC.thy"
unused file
"/home/makarius/isabelle/repos/AFP/thys/Pi_Calculus/Strong_Late_Sim_bak.thy"
unused file
"/home/makarius/isabelle/repos/AFP/thys/Pi_Calculus/Weak_Early_Bisim_Subst_Pres.thy"
unused file
"/home/makarius/isabelle/repos/AFP/thys/Pi_Calculus/Weak_Early_Bisim_Subst_SC.thy"
unused file
"/home/makarius/isabelle/repos/AFP/thys/Pi_Calculus/Weak_Early_Cong_SC.thy"
unused file
"/home/makarius/isabelle/repos/AFP/thys/Pi_Calculus/Weak_Early_Cong_Subst_SC.thy"
unused file
"/home/makarius/isabelle/repos/AFP/thys/Pi_Calculus/Weak_Early_Late_Comp.thy"
unused file
"/home/makarius/isabelle/repos/AFP/thys/Pi_Calculus/Weak_Late_Bisim_Subst_Pres.thy"
unused file
"/home/makarius/isabelle/repos/AFP/thys/Pi_Calculus/Weak_Late_Bisim_Subst_SC.thy"
unused file
"/home/makarius/isabelle/repos/AFP/thys/Pi_Calculus/Weak_Late_Cong_SC.thy"
unused file
"/home/makarius/isabelle/repos/AFP/thys/Pi_Calculus/Weak_Late_Cong_Subst_Pres.thy"
unused file
"/home/makarius/isabelle/repos/AFP/thys/Polynomial_Factorization/External_Factorization.thy"
unused file
"/home/makarius/isabelle/repos/AFP/thys/Polynomial_Factorization/Hybrid_Factorization.thy"
unused file
"/home/makarius/isabelle/repos/AFP/thys/Psi_Calculi/Weak_Bisim_Subst.thy"
unused file
"/home/makarius/isabelle/repos/AFP/thys/Psi_Calculi/Weak_Semantics.thy"
unused file
"/home/makarius/isabelle/repos/AFP/thys/Routing/ReversePathFiltering.thy"
unused file
"/home/makarius/isabelle/repos/AFP/thys/Simpl/DPC0Expressions.thy"
unused file "/home/makarius/isabelle/repos/AFP/thys/Simpl/DPC0Library.thy"
unused file
"/home/makarius/isabelle/repos/AFP/thys/Stable_Matching/Nitpick.thy"
Maybe some AFP authors or editors want to sort this out ...
Makarius
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
