[
      {"Well_Quasi_Orders":
        {"distrib_deps": ["HOL-Library"],
         "afp_deps": ["Abstract-Rewriting", "Open_Induction"]
        }
      }, 
      {"Nested_Multisets_Ordinals":
        {"distrib_deps": ["HOL-Library"],
         "afp_deps": ["List-Index", "Ordinal"]
        }
      }, 
      {"Sturm_Tarski":
        {"distrib_deps": ["HOL-Computational_Algebra"],
         "afp_deps": []
        }
      }, 
      {"Prime_Number_Theorem":
        {"distrib_deps": ["HOL-Real_Asymp"],
         "afp_deps": ["Stirling_Formula", "Zeta_Function"]
        }
      }, 
      {"Jordan_Normal_Form":
        {"distrib_deps": [],
         "afp_deps": ["Polynomial_Factorization"]
        }
      }, 
      {"LLL_Factorization":
        {"distrib_deps": [],
         "afp_deps": ["LLL_Basis_Reduction", "Perron_Frobenius"]
        }
      }, 
      {"Program-Conflict-Analysis":
        {"distrib_deps": ["HOL-Library"],
         "afp_deps": []
        }
      }, 
      {"CryptoBasedCompositionalProperties":
        {"distrib_deps": ["HOL"],
         "afp_deps": []
        }
      }, 
      {"Cauchy":
        {"distrib_deps": ["HOL"],
         "afp_deps": []
        }
      }, 
      {"Password_Authentication_Protocol":
        {"distrib_deps": ["HOL-Library"],
         "afp_deps": []
        }
      }, 
      {"Nat-Interval-Logic":
        {"distrib_deps": [],
         "afp_deps": ["List-Infinite"]
        }
      }, 
      {"Decreasing-Diagrams":
        {"distrib_deps": [],
         "afp_deps": ["Abstract-Rewriting"]
        }
      }, 
      {"MSO_Regex_Equivalence":
        {"distrib_deps": ["HOL", "HOL-Library"],
         "afp_deps": ["Deriving", "List-Index"]
        }
      }, 
      {"Certification_Monads":
        {"distrib_deps": ["HOL", "HOL-Library"],
         "afp_deps": ["Partial_Function_MR", "Show"]
        }
      }, 
      {"Paraconsistency":
        {"distrib_deps": ["HOL"],
         "afp_deps": []
        }
      }, 
      {"List_Update":
        {"distrib_deps": ["HOL-Probability"],
         "afp_deps": ["List-Index", "Regular-Sets"]
        }
      }, 
      {"Matrix":
        {"distrib_deps": ["HOL-Algebra"],
         "afp_deps": ["Abstract-Rewriting"]
        }
      }, 
      {"Category3":
        {"distrib_deps": ["HOL-Library"],
         "afp_deps": []
        }
      }, 
      {"Tail_Recursive_Functions":
        {"distrib_deps": ["HOL-Library"],
         "afp_deps": []
        }
      }, 
      {"UPF_Firewall":
        {"distrib_deps": [],
         "afp_deps": ["UPF"]
        }
      }, 
      {"Card_Number_Partitions":
        {"distrib_deps": ["HOL-Library"],
         "afp_deps": []
        }
      }, 
      {"Priority_Queue_Braun":
        {"distrib_deps": ["HOL-Data_Structures", "HOL-Library"],
         "afp_deps": []
        }
      }, 
      {"Prime_Distribution_Elementary":
        {"distrib_deps": [],
         "afp_deps": ["Prime_Number_Theorem", "Zeta_Function"]
        }
      }, 
      {"Sturm_Sequences":
        {"distrib_deps": ["HOL-Computational_Algebra"],
         "afp_deps": []
        }
      }, 
      {"Jordan_Hoelder":
        {"distrib_deps": ["HOL-Algebra"],
         "afp_deps": ["Secondary_Sylow"]
        }
      }, 
      {"Abstract-Rewriting":
        {"distrib_deps": ["HOL-Library"],
         "afp_deps": ["Regular-Sets"]
        }
      }, 
      {"Stirling_Formula":
        {"distrib_deps": ["HOL-Analysis"],
         "afp_deps": ["Bernoulli", "Landau_Symbols"]
        }
      }, 
      {"Abstract-Hoare-Logics":
        {"distrib_deps": ["HOL"],
         "afp_deps": []
        }
      }, 
      {"Monad_Normalisation":
        {"distrib_deps": ["HOL-Probability"],
         "afp_deps": []
        }
      }, 
      {"Graph_Theory":
        {"distrib_deps": ["HOL-Library"],
         "afp_deps": []
        }
      }, 
      {"CakeML":
        {"distrib_deps": ["HOL-Word"],
         "afp_deps": ["Coinductive", "IEEE_Floating_Point", "Show"]
        }
      }, 
      {"Triangle":
        {"distrib_deps": ["HOL-Analysis"],
         "afp_deps": []
        }
      }, 
      {"Ribbon_Proofs":
        {"distrib_deps": ["HOL-Library"],
         "afp_deps": []
        }
      }, 
      {"OpSets":
        {"distrib_deps": ["HOL"],
         "afp_deps": []
        }
      }, 
      {"Coinductive":
        {"distrib_deps": ["HOL-Analysis", "HOL-Computational_Algebra"],
         "afp_deps": []
        }
      }, 
      {"PCF":
        {"distrib_deps": ["HOLCF-Library"],
         "afp_deps": []
        }
      }, 
      {"Abs_Int_ITP2012":
        {"distrib_deps": ["HOL-IMP", "HOL-Library"],
         "afp_deps": []
        }
      }, 
      {"Consensus_Refined":
        {"distrib_deps": ["HOL", "HOL-Library"],
         "afp_deps": ["Heard_Of", "Stuttering_Equivalence"]
        }
      }, 
      {"WorkerWrapper":
        {"distrib_deps": ["HOLCF"],
         "afp_deps": []
        }
      }, 
      {"CYK":
        {"distrib_deps": ["HOL"],
         "afp_deps": []
        }
      }, 
      {"LTL_to_DRA":
        {"distrib_deps": [],
         "afp_deps": ["Boolean_Expression_Checkers", "KBPs", "LTL", "List-Index"]
        }
      }, 
      {"TortoiseHare":
        {"distrib_deps": ["HOL-Library"],
         "afp_deps": []
        }
      }, 
      {"Free-Groups":
        {"distrib_deps": ["HOL", "HOL-Algebra", "HOL-Cardinals", "HOL-Computational_Algebra"],
         "afp_deps": ["Applicative_Lifting"]
        }
      }, 
      {"FunWithTilings":
        {"distrib_deps": ["HOL"],
         "afp_deps": []
        }
      }, 
      {"Aggregation_Algebras":
        {"distrib_deps": [],
         "afp_deps": ["Stone_Kleene_Relation_Algebras"]
        }
      }, 
      {"Heard_Of":
        {"distrib_deps": ["HOL", "HOL-Library"],
         "afp_deps": ["Stuttering_Equivalence"]
        }
      }, 
      {"Decl_Sem_Fun_PL":
        {"distrib_deps": ["HOL", "HOL-Library"],
         "afp_deps": []
        }
      }, 
      {"Transformer_Semantics":
        {"distrib_deps": [],
         "afp_deps": ["Order_Lattice_Props", "Quantales"]
        }
      }, 
      {"No_FTL_observers":
        {"distrib_deps": ["HOL"],
         "afp_deps": []
        }
      }, 
      {"Functional-Automata":
        {"distrib_deps": ["HOL-Library"],
         "afp_deps": ["Regular-Sets"]
        }
      }, 
      {"CISC-Kernel":
        {"distrib_deps": ["HOL"],
         "afp_deps": []
        }
      }, 
      {"Verified-Prover":
        {"distrib_deps": ["HOL"],
         "afp_deps": []
        }
      }, 
      {"DynamicArchitectures":
        {"distrib_deps": [],
         "afp_deps": ["Coinductive"]
        }
      }, 
      {"Subresultants":
        {"distrib_deps": [],
         "afp_deps": ["Jordan_Normal_Form", "Polynomial_Factorization"]
        }
      }, 
      {"LTL":
        {"distrib_deps": ["HOL-Library"],
         "afp_deps": ["Boolean_Expression_Checkers"]
        }
      }, 
      {"Lazy-Lists-II":
        {"distrib_deps": [],
         "afp_deps": ["Coinductive"]
        }
      }, 
      {"Abstract_Soundness":
        {"distrib_deps": [],
         "afp_deps": ["Abstract_Completeness"]
        }
      }, 
      {"General-Triangle":
        {"distrib_deps": ["HOL"],
         "afp_deps": []
        }
      }, 
      {"Euler_Partition":
        {"distrib_deps": ["HOL", "HOL-Library"],
         "afp_deps": ["Card_Number_Partitions"]
        }
      }, 
      {"Lifting_Definition_Option":
        {"distrib_deps": ["HOL"],
         "afp_deps": []
        }
      }, 
      {"Depth-First-Search":
        {"distrib_deps": ["HOL"],
         "afp_deps": []
        }
      }, 
      {"Prpu_Maxflow":
        {"distrib_deps": [],
         "afp_deps": ["Flow_Networks"]
        }
      }, 
      {"SIFPL":
        {"distrib_deps": ["HOL"],
         "afp_deps": []
        }
      }, 
      {"Twelvefold_Way":
        {"distrib_deps": ["HOL-Eisbach", "HOL-Library", "HOL-ex"],
         "afp_deps": ["Bell_Numbers_Spivey", "Card_Multisets", "Card_Number_Partitions", "Card_Partitions"]
        }
      }, 
      {"JinjaThreads":
        {"distrib_deps": ["HOL", "HOL-Word"],
         "afp_deps": ["Automatic_Refinement", "Binomial-Heaps", "Coinductive", "Collections", "FinFun", "Finger-Trees", "Native_Word", "Refine_Monadic", "Trie"]
        }
      }, 
      {"Tree-Automata":
        {"distrib_deps": [],
         "afp_deps": ["Collections"]
        }
      }, 
      {"Knuth_Morris_Pratt":
        {"distrib_deps": [],
         "afp_deps": ["Refine_Imperative_HOL"]
        }
      }, 
      {"Noninterference_CSP":
        {"distrib_deps": ["HOL"],
         "afp_deps": []
        }
      }, 
      {"Mason_Stothers":
        {"distrib_deps": ["HOL-Computational_Algebra"],
         "afp_deps": []
        }
      }, 
      {"Category2":
        {"distrib_deps": ["HOL-Library", "HOL-ZF"],
         "afp_deps": []
        }
      }, 
      {"First_Order_Terms":
        {"distrib_deps": ["HOL-Library"],
         "afp_deps": ["Abstract-Rewriting"]
        }
      }, 
      {"PLM":
        {"distrib_deps": ["HOL", "HOL-Eisbach", "HOL-Library"],
         "afp_deps": []
        }
      }, 
      {"Gabow_SCC":
        {"distrib_deps": [],
         "afp_deps": ["CAVA_Automata"]
        }
      }, 
      {"DataRefinementIBP":
        {"distrib_deps": ["HOL"],
         "afp_deps": ["LatticeProperties"]
        }
      }, 
      {"Bounded_Deducibility_Security":
        {"distrib_deps": ["HOL"],
         "afp_deps": []
        }
      }, 
      {"Hybrid_Multi_Lane_Spatial_Logic":
        {"distrib_deps": ["HOL"],
         "afp_deps": []
        }
      }, 
      {"Ordered_Resolution_Prover":
        {"distrib_deps": ["HOL-Library"],
         "afp_deps": ["Coinductive", "Nested_Multisets_Ordinals"]
        }
      }, 
      {"Bondy":
        {"distrib_deps": ["HOL"],
         "afp_deps": []
        }
      }, 
      {"Containers":
        {"distrib_deps": [],
         "afp_deps": ["Automatic_Refinement", "Collections", "Deriving", "Finger-Trees", "Regular-Sets", "Trie"]
        }
      }, 
      {"Echelon_Form":
        {"distrib_deps": ["HOL-Analysis"],
         "afp_deps": ["Cayley_Hamilton", "Gauss_Jordan", "Rank_Nullity_Theorem"]
        }
      }, 
      {"Simple_Firewall":
        {"distrib_deps": [],
         "afp_deps": ["IP_Addresses"]
        }
      }, 
      {"Dependent_SIFUM_Refinement":
        {"distrib_deps": ["HOL-Eisbach"],
         "afp_deps": ["Dependent_SIFUM_Type_Systems"]
        }
      }, 
      {"Stone_Algebras":
        {"distrib_deps": ["HOL"],
         "afp_deps": []
        }
      }, 
      {"Abortable_Linearizable_Modules":
        {"distrib_deps": ["HOL"],
         "afp_deps": []
        }
      }, 
      {"Lowe_Ontological_Argument":
        {"distrib_deps": ["HOL"],
         "afp_deps": []
        }
      }, 
      {"Minimal_SSA":
        {"distrib_deps": [],
         "afp_deps": ["Formal_SSA"]
        }
      }, 
      {"UpDown_Scheme":
        {"distrib_deps": ["HOL-Analysis", "HOL-Imperative_HOL"],
         "afp_deps": ["Automatic_Refinement", "Separation_Logic_Imperative_HOL"]
        }
      }, 
      {"HereditarilyFinite":
        {"distrib_deps": ["HOL-Library"],
         "afp_deps": []
        }
      }, 
      {"Stochastic_Matrices":
        {"distrib_deps": [],
         "afp_deps": ["Jordan_Normal_Form", "Markov_Models", "Perron_Frobenius"]
        }
      }, 
      {"Menger":
        {"distrib_deps": ["HOL"],
         "afp_deps": []
        }
      }, 
      {"Inductive_Confidentiality":
        {"distrib_deps": ["HOL"],
         "afp_deps": []
        }
      }, 
      {"Gromov_Hyperbolicity":
        {"distrib_deps": ["HOL-Analysis", "HOL-Cardinals", "HOL-Decision_Procs"],
         "afp_deps": ["Ergodic_Theory"]
        }
      }, 
      {"KAD":
        {"distrib_deps": ["HOL"],
         "afp_deps": ["Kleene_Algebra"]
        }
      }, 
      {"List-Infinite":
        {"distrib_deps": ["HOL-Library"],
         "afp_deps": []
        }
      }, 
      {"Statecharts":
        {"distrib_deps": ["HOL"],
         "afp_deps": []
        }
      }, 
      {"Median_Of_Medians_Selection":
        {"distrib_deps": ["HOL", "HOL-Library"],
         "afp_deps": []
        }
      }, 
      {"VectorSpace":
        {"distrib_deps": ["HOL-Algebra"],
         "afp_deps": []
        }
      }, 
      {"Universal_Turing_Machine":
        {"distrib_deps": ["HOL"],
         "afp_deps": []
        }
      }, 
      {"Separation_Logic_Imperative_HOL":
        {"distrib_deps": ["HOL-Imperative_HOL", "HOL-Library", "HOL-Word", "HOL-ex"],
         "afp_deps": ["Automatic_Refinement", "Collections", "Native_Word"]
        }
      }, 
      {"CAVA_Automata":
        {"distrib_deps": [],
         "afp_deps": ["Collections", "Deriving"]
        }
      }, 
      {"Amortized_Complexity":
        {"distrib_deps": ["HOL-Library"],
         "afp_deps": ["Pairing_Heap", "Skew_Heap", "Splay_Tree"]
        }
      }, 
      {"Dynamic_Tables":
        {"distrib_deps": [],
         "afp_deps": ["Amortized_Complexity"]
        }
      }, 
      {"Resolution_FOL":
        {"distrib_deps": ["HOL", "HOL-Library"],
         "afp_deps": ["First_Order_Terms"]
        }
      }, 
      {"Constructive_Cryptography":
        {"distrib_deps": [],
         "afp_deps": ["CryptHOL"]
        }
      }, 
      {"Pop_Refinement":
        {"distrib_deps": ["HOL"],
         "afp_deps": []
        }
      }, 
      {"Deriving":
        {"distrib_deps": ["HOL-Library", "HOL-Word"],
         "afp_deps": ["Collections", "Native_Word"]
        }
      }, 
      {"MonoidalCategory":
        {"distrib_deps": [],
         "afp_deps": ["Category3"]
        }
      }, 
      {"Vickrey_Clarke_Groves":
        {"distrib_deps": ["HOL-Library"],
         "afp_deps": []
        }
      }, 
      {"Ergodic_Theory":
        {"distrib_deps": ["HOL-Probability"],
         "afp_deps": []
        }
      }, 
      {"Real_Impl":
        {"distrib_deps": ["HOL-Computational_Algebra"],
         "afp_deps": ["Deriving", "Show", "Sqrt_Babylonian"]
        }
      }, 
      {"HOLCF-Prelude":
        {"distrib_deps": ["HOL-Computational_Algebra", "HOLCF", "HOLCF-Library"],
         "afp_deps": []
        }
      }, 
      {"Berlekamp_Zassenhaus":
        {"distrib_deps": ["HOL-Number_Theory", "HOL-Types_To_Sets", "HOL-Word"],
         "afp_deps": ["Efficient-Mergesort", "Polynomial_Factorization", "Polynomial_Interpolation", "Show", "Subresultants"]
        }
      }, 
      {"Signature_Groebner":
        {"distrib_deps": [],
         "afp_deps": ["Groebner_Bases"]
        }
      }, 
      {"Efficient-Mergesort":
        {"distrib_deps": ["HOL-Library"],
         "afp_deps": []
        }
      }, 
      {"Pell":
        {"distrib_deps": ["HOL-Computational_Algebra", "HOL-Library"],
         "afp_deps": []
        }
      }, 
      {"Binomial-Heaps":
        {"distrib_deps": ["HOL-Library"],
         "afp_deps": []
        }
      }, 
      {"Separation_Algebra":
        {"distrib_deps": ["HOL-Hoare", "HOL-Word"],
         "afp_deps": []
        }
      }, 
      {"SDS_Impossibility":
        {"distrib_deps": [],
         "afp_deps": ["Randomised_Social_Choice"]
        }
      }, 
      {"Cayley_Hamilton":
        {"distrib_deps": ["HOL-Analysis"],
         "afp_deps": []
        }
      }, 
      {"Stuttering_Equivalence":
        {"distrib_deps": [],
         "afp_deps": ["LTL"]
        }
      }, 
      {"Complx":
        {"distrib_deps": [],
         "afp_deps": ["Word_Lib"]
        }
      }, 
      {"Octonions":
        {"distrib_deps": ["HOL-Analysis"],
         "afp_deps": []
        }
      }, 
      {"Proof_Strategy_Language":
        {"distrib_deps": ["HOL", "HOL-Eisbach"],
         "afp_deps": []
        }
      }, 
      {"Orbit_Stabiliser":
        {"distrib_deps": ["HOL-Algebra"],
         "afp_deps": []
        }
      }, 
      {"Simplex":
        {"distrib_deps": ["HOL-Library"],
         "afp_deps": []
        }
      }, 
      {"Lehmer":
        {"distrib_deps": ["HOL-Number_Theory"],
         "afp_deps": []
        }
      }, 
      {"DPT-SAT-Solver":
        {"distrib_deps": ["HOL"],
         "afp_deps": []
        }
      }, 
      {"Compiling-Exceptions-Correctly":
        {"distrib_deps": ["HOL"],
         "afp_deps": []
        }
      }, 
      {"InfPathElimination":
        {"distrib_deps": ["HOL"],
         "afp_deps": []
        }
      }, 
      {"Probabilistic_System_Zoo":
        {"distrib_deps": ["HOL-Cardinals", "HOL-Eisbach", "HOL-Probability", "HOL-Analysis"],
         "afp_deps": []
        }
      }, 
      {"Prime_Harmonic_Series":
        {"distrib_deps": ["HOL-Analysis", "HOL-Number_Theory"],
         "afp_deps": []
        }
      }, 
      {"Launchbury":
        {"distrib_deps": ["HOLCF"],
         "afp_deps": ["FinFun", "Nominal2"]
        }
      }, 
      {"Fisher_Yates":
        {"distrib_deps": ["HOL-Probability"],
         "afp_deps": []
        }
      }, 
      {"FLP":
        {"distrib_deps": ["HOL"],
         "afp_deps": []
        }
      }, 
      {"VerifyThis2018":
        {"distrib_deps": [],
         "afp_deps": ["Refine_Imperative_HOL"]
        }
      }, 
      {"Store_Buffer_Reduction":
        {"distrib_deps": ["HOL"],
         "afp_deps": []
        }
      }, 
      {"Lambda_Free_EPO":
        {"distrib_deps": ["HOL-Library"],
         "afp_deps": ["Lambda_Free_RPOs"]
        }
      }, 
      {"Formal_SSA":
        {"distrib_deps": [],
         "afp_deps": ["CAVA_Automata", "Collections", "Dijkstra_Shortest_Path", "Slicing"]
        }
      }, 
      {"GewirthPGCProof":
        {"distrib_deps": ["HOL"],
         "afp_deps": []
        }
      }, 
      {"Discrete_Summation":
        {"distrib_deps": ["HOL", "HOL-Library"],
         "afp_deps": []
        }
      }, 
      {"Floyd_Warshall":
        {"distrib_deps": [],
         "afp_deps": ["Refine_Imperative_HOL"]
        }
      }, 
      {"KAT_and_DRA":
        {"distrib_deps": [],
         "afp_deps": ["Kleene_Algebra"]
        }
      }, 
      {"ROBDD":
        {"distrib_deps": ["HOL-Imperative_HOL", "HOL-Library", "HOL-Word", "HOL-ex"],
         "afp_deps": ["Automatic_Refinement", "Collections", "Native_Word", "Refine_Imperative_HOL"]
        }
      }, 
      {"Formula_Derivatives":
        {"distrib_deps": ["HOL-Library"],
         "afp_deps": ["Coinductive_Languages", "Deriving", "List-Index", "Show"]
        }
      }, 
      {"GraphMarkingIBP":
        {"distrib_deps": ["HOL"],
         "afp_deps": ["DataRefinementIBP"]
        }
      }, 
      {"CAVA_LTL_Modelchecker":
        {"distrib_deps": [],
         "afp_deps": ["CAVA_Automata", "Gabow_SCC", "LTL_to_GBA", "Promela", "DFS_Framework", "Partial_Order_Reduction"]
        }
      }, 
      {"Stone_Relation_Algebras":
        {"distrib_deps": [],
         "afp_deps": ["Stone_Algebras"]
        }
      }, 
      {"IMAP-CRDT":
        {"distrib_deps": [],
         "afp_deps": ["CRDT"]
        }
      }, 
      {"Treaps":
        {"distrib_deps": ["HOL-Library", "HOL-Probability"],
         "afp_deps": ["Comparison_Sort_Lower_Bound", "Random_BSTs"]
        }
      }, 
      {"Weight_Balanced_Trees":
        {"distrib_deps": ["HOL", "HOL-Data_Structures", "HOL-Library"],
         "afp_deps": []
        }
      }, 
      {"SIFUM_Type_Systems":
        {"distrib_deps": ["HOL", "HOL-Library"],
         "afp_deps": []
        }
      }, 
      {"Integration":
        {"distrib_deps": ["HOL-Library"],
         "afp_deps": []
        }
      }, 
      {"FileRefinement":
        {"distrib_deps": ["HOL"],
         "afp_deps": []
        }
      }, 
      {"Liouville_Numbers":
        {"distrib_deps": ["HOL-Computational_Algebra"],
         "afp_deps": []
        }
      }, 
      {"LTL_to_GBA":
        {"distrib_deps": [],
         "afp_deps": ["CAVA_Automata", "LTL", "Stuttering_Equivalence"]
        }
      }, 
      {"Case_Labeling":
        {"distrib_deps": ["HOL", "HOL-Eisbach", "HOL-Hoare"],
         "afp_deps": []
        }
      }, 
      {"Polynomial_Factorization":
        {"distrib_deps": ["HOL-Algebra", "HOL-Cardinals"],
         "afp_deps": ["Abstract-Rewriting", "Containers", "Gauss_Jordan", "Matrix", "Polynomial_Interpolation", "Show", "VectorSpace", "Partial_Function_MR", "Sqrt_Babylonian"]
        }
      }, 
      {"Tarskis_Geometry":
        {"distrib_deps": ["HOL-Algebra", "HOL-Analysis"],
         "afp_deps": []
        }
      }, 
      {"Akra_Bazzi":
        {"distrib_deps": ["HOL-Analysis", "HOL-Decision_Procs"],
         "afp_deps": ["Landau_Symbols"]
        }
      }, 
      {"BinarySearchTree":
        {"distrib_deps": ["HOL"],
         "afp_deps": []
        }
      }, 
      {"Lazy_Case":
        {"distrib_deps": ["HOL"],
         "afp_deps": []
        }
      }, 
      {"Surprise_Paradox":
        {"distrib_deps": [],
         "afp_deps": ["Incompleteness"]
        }
      }, 
      {"Neumann_Morgenstern_Utility":
        {"distrib_deps": ["HOL-Probability"],
         "afp_deps": ["First_Welfare_Theorem"]
        }
      }, 
      {"Stream-Fusion":
        {"distrib_deps": ["HOLCF", "HOLCF-Library"],
         "afp_deps": []
        }
      }, 
      {"Comparison_Sort_Lower_Bound":
        {"distrib_deps": [],
         "afp_deps": ["Landau_Symbols", "List-Index", "Stirling_Formula"]
        }
      }, 
      {"Auto2_Imperative_HOL":
        {"distrib_deps": ["HOL-Imperative_HOL", "HOL-Library"],
         "afp_deps": ["Auto2_HOL"]
        }
      }, 
      {"IP_Addresses":
        {"distrib_deps": ["HOL-ex"],
         "afp_deps": ["Automatic_Refinement", "Word_Lib"]
        }
      }, 
      {"Dijkstra_Shortest_Path":
        {"distrib_deps": [],
         "afp_deps": ["Collections"]
        }
      }, 
      {"Derangements":
        {"distrib_deps": ["HOL", "HOL-Library"],
         "afp_deps": []
        }
      }, 
      {"PseudoHoops":
        {"distrib_deps": ["HOL"],
         "afp_deps": ["LatticeProperties"]
        }
      }, 
      {"Stern_Brocot":
        {"distrib_deps": [],
         "afp_deps": ["Applicative_Lifting"]
        }
      }, 
      {"Open_Induction":
        {"distrib_deps": ["HOL"],
         "afp_deps": []
        }
      }, 
      {"UTP":
        {"distrib_deps": ["HOL-Algebra"],
         "afp_deps": ["Optics"]
        }
      }, 
      {"Regex_Equivalence":
        {"distrib_deps": ["HOL", "HOL-Library", "Spec_Check"],
         "afp_deps": ["Efficient-Mergesort", "Regular-Sets"]
        }
      }, 
      {"IEEE_Floating_Point":
        {"distrib_deps": ["HOL-Library"],
         "afp_deps": ["Word_Lib"]
        }
      }, 
      {"SPARCv8":
        {"distrib_deps": ["HOL-Eisbach", "HOL-Word"],
         "afp_deps": []
        }
      }, 
      {"Simpl":
        {"distrib_deps": ["HOL", "HOL-Library", "HOL-Statespace"],
         "afp_deps": []
        }
      }, 
      {"Regular-Sets":
        {"distrib_deps": ["HOL-Library"],
         "afp_deps": []
        }
      }, 
      {"InformationFlowSlicing_Inter":
        {"distrib_deps": [],
         "afp_deps": ["HRB-Slicing"]
        }
      }, 
      {"Higher_Order_Terms":
        {"distrib_deps": ["HOL", "HOL-ex"],
         "afp_deps": ["Datatype_Order_Generator", "Lambda_Free_RPOs", "List-Index"]
        }
      }, 
      {"DFS_Framework":
        {"distrib_deps": [],
         "afp_deps": ["CAVA_Automata"]
        }
      }, 
      {"Dirichlet_L":
        {"distrib_deps": ["HOL-Algebra", "HOL-Analysis", "HOL-Library"],
         "afp_deps": ["Bertrands_Postulate", "Dirichlet_Series", "Landau_Symbols", "Zeta_Function"]
        }
      }, 
      {"List-Index":
        {"distrib_deps": ["HOL"],
         "afp_deps": []
        }
      }, 
      {"Randomised_Social_Choice":
        {"distrib_deps": ["HOL-Probability"],
         "afp_deps": ["List-Index"]
        }
      }, 
      {"Euler_MacLaurin":
        {"distrib_deps": ["HOL-Analysis"],
         "afp_deps": ["Bernoulli", "Landau_Symbols"]
        }
      }, 
      {"Show":
        {"distrib_deps": ["HOL-Computational_Algebra"],
         "afp_deps": ["Datatype_Order_Generator", "Deriving"]
        }
      }, 
      {"WHATandWHERE_Security":
        {"distrib_deps": ["HOL"],
         "afp_deps": ["Strong_Security"]
        }
      }, 
      {"Partial_Order_Reduction":
        {"distrib_deps": [],
         "afp_deps": ["Coinductive", "Stuttering_Equivalence", "Transition_Systems_and_Automata"]
        }
      }, 
      {"Rep_Fin_Groups":
        {"distrib_deps": ["HOL-Computational_Algebra"],
         "afp_deps": []
        }
      }, 
      {"Root_Balanced_Tree":
        {"distrib_deps": ["HOL-Data_Structures", "HOL-Decision_Procs", "HOL-Library"],
         "afp_deps": ["Amortized_Complexity"]
        }
      }, 
      {"Descartes_Sign_Rule":
        {"distrib_deps": ["HOL-Computational_Algebra"],
         "afp_deps": []
        }
      }, 
      {"Noninterference_Ipurge_Unwinding":
        {"distrib_deps": [],
         "afp_deps": ["List_Interleaving", "Noninterference_CSP"]
        }
      }, 
      {"Markov_Models":
        {"distrib_deps": ["HOL-Probability"],
         "afp_deps": ["Coinductive", "Gauss-Jordan-Elim-Fun"]
        }
      }, 
      {"POPLmark-deBruijn":
        {"distrib_deps": ["HOL-Library"],
         "afp_deps": []
        }
      }, 
      {"Matroids":
        {"distrib_deps": ["HOL"],
         "afp_deps": []
        }
      }, 
      {"Cartan_FP":
        {"distrib_deps": ["HOL-Analysis"],
         "afp_deps": []
        }
      }, 
      {"Timed_Automata":
        {"distrib_deps": ["HOL"],
         "afp_deps": []
        }
      }, 
      {"Jinja":
        {"distrib_deps": ["HOL-Library"],
         "afp_deps": ["List-Index"]
        }
      }, 
      {"Example-Submission":
        {"distrib_deps": ["HOL"],
         "afp_deps": []
        }
      }, 
      {"Hoare_Time":
        {"distrib_deps": ["HOL", "HOL-Eisbach", "HOL-Library"],
         "afp_deps": ["Separation_Algebra"]
        }
      }, 
      {"Monad_Memo_DP":
        {"distrib_deps": ["HOL", "HOL-Eisbach", "HOL-Imperative_HOL", "HOL-Library"],
         "afp_deps": ["Show"]
        }
      }, 
      {"Isabelle_Meta_Model":
        {"distrib_deps": ["HOL-Library"],
         "afp_deps": []
        }
      }, 
      {"Recursion-Theory-I":
        {"distrib_deps": ["HOL"],
         "afp_deps": []
        }
      }, 
      {"Word_Lib":
        {"distrib_deps": ["HOL-Word"],
         "afp_deps": []
        }
      }, 
      {"Refine_Imperative_HOL":
        {"distrib_deps": ["HOL-Eisbach", "Isar_Ref", "HOL-Imperative_HOL", "HOL-Library"],
         "afp_deps": ["Collections", "DFS_Framework", "Dijkstra_Shortest_Path", "List-Index", "Separation_Logic_Imperative_HOL"]
        }
      }, 
      {"Localization_Ring":
        {"distrib_deps": ["HOL-Algebra"],
         "afp_deps": []
        }
      }, 
      {"Collections":
        {"distrib_deps": [],
         "afp_deps": ["Binomial-Heaps", "Finger-Trees", "Native_Word", "Refine_Monadic", "Trie", "CAVA_Automata", "Containers"]
        }
      }, 
      {"Bernoulli":
        {"distrib_deps": ["HOL-Analysis"],
         "afp_deps": []
        }
      }, 
      {"Sqrt_Babylonian":
        {"distrib_deps": [],
         "afp_deps": ["Cauchy"]
        }
      }, 
      {"Minkowskis_Theorem":
        {"distrib_deps": ["HOL-Analysis"],
         "afp_deps": []
        }
      }, 
      {"Girth_Chromatic":
        {"distrib_deps": ["HOL-Decision_Procs", "HOL-Library", "HOL-Probability"],
         "afp_deps": []
        }
      }, 
      {"TLA":
        {"distrib_deps": ["HOL"],
         "afp_deps": []
        }
      }, 
      {"Error_Function":
        {"distrib_deps": ["HOL-Analysis"],
         "afp_deps": ["Landau_Symbols"]
        }
      }, 
      {"NormByEval":
        {"distrib_deps": ["HOL"],
         "afp_deps": []
        }
      }, 
      {"Quaternions":
        {"distrib_deps": ["HOL-Analysis"],
         "afp_deps": []
        }
      }, 
      {"BDD":
        {"distrib_deps": [],
         "afp_deps": ["Simpl"]
        }
      }, 
      {"Fermat3_4":
        {"distrib_deps": ["HOL-Number_Theory"],
         "afp_deps": []
        }
      }, 
      {"LocalLexing":
        {"distrib_deps": ["HOL"],
         "afp_deps": []
        }
      }, 
      {"Datatype_Order_Generator":
        {"distrib_deps": ["HOL-Library", "HOL-Word"],
         "afp_deps": ["Deriving", "Native_Word"]
        }
      }, 
      {"Sort_Encodings":
        {"distrib_deps": ["HOL-Cardinals"],
         "afp_deps": []
        }
      }, 
      {"AWN":
        {"distrib_deps": ["HOL"],
         "afp_deps": []
        }
      }, 
      {"Random_Graph_Subgraph_Threshold":
        {"distrib_deps": [],
         "afp_deps": ["Girth_Chromatic"]
        }
      }, 
      {"PropResPI":
        {"distrib_deps": ["HOL"],
         "afp_deps": []
        }
      }, 
      {"Native_Word":
        {"distrib_deps": ["HOL-Imperative_HOL", "HOL-Word"],
         "afp_deps": []
        }
      }, 
      {"GPU_Kernel_PL":
        {"distrib_deps": ["HOL"],
         "afp_deps": []
        }
      }, 
      {"ConcurrentGC":
        {"distrib_deps": [],
         "afp_deps": ["ConcurrentIMP"]
        }
      }, 
      {"CoreC++":
        {"distrib_deps": ["HOL-Library"],
         "afp_deps": []
        }
      }, 
      {"ComponentDependencies":
        {"distrib_deps": ["HOL"],
         "afp_deps": []
        }
      }, 
      {"Routing":
        {"distrib_deps": [],
         "afp_deps": ["Simple_Firewall"]
        }
      }, 
      {"Card_Equiv_Relations":
        {"distrib_deps": [],
         "afp_deps": ["Bell_Numbers_Spivey"]
        }
      }, 
      {"LatticeProperties":
        {"distrib_deps": ["HOL"],
         "afp_deps": []
        }
      }, 
      {"Winding_Number_Eval":
        {"distrib_deps": ["HOL-Analysis", "HOL-Computational_Algebra", "HOL-Eisbach"],
         "afp_deps": ["Budan_Fourier", "Sturm_Tarski"]
        }
      }, 
      {"Noninterference_Inductive_Unwinding":
        {"distrib_deps": ["HOL"],
         "afp_deps": ["Noninterference_Ipurge_Unwinding"]
        }
      }, 
      {"LambdaMu":
        {"distrib_deps": ["HOL"],
         "afp_deps": []
        }
      }, 
      {"Robbins-Conjecture":
        {"distrib_deps": ["HOL"],
         "afp_deps": []
        }
      }, 
      {"Lower_Semicontinuous":
        {"distrib_deps": ["HOL-Analysis"],
         "afp_deps": []
        }
      }, 
      {"Algebraic_Numbers":
        {"distrib_deps": [],
         "afp_deps": ["Berlekamp_Zassenhaus", "Sturm_Sequences"]
        }
      }, 
      {"Group-Ring-Module":
        {"distrib_deps": ["HOL-Library"],
         "afp_deps": []
        }
      }, 
      {"Taylor_Models":
        {"distrib_deps": [],
         "afp_deps": ["Affine_Arithmetic"]
        }
      }, 
      {"Lambda_Free_RPOs":
        {"distrib_deps": ["HOL-Cardinals", "HOL-Library"],
         "afp_deps": []
        }
      }, 
      {"SumSquares":
        {"distrib_deps": ["HOL-Number_Theory"],
         "afp_deps": []
        }
      }, 
      {"LLL_Basis_Reduction":
        {"distrib_deps": [],
         "afp_deps": ["Algebraic_Numbers", "Berlekamp_Zassenhaus", "Perron_Frobenius"]
        }
      }, 
      {"ConcurrentIMP":
        {"distrib_deps": ["HOL-Library"],
         "afp_deps": []
        }
      }, 
      {"Category":
        {"distrib_deps": ["HOL", "HOL-Library"],
         "afp_deps": []
        }
      }, 
      {"Kleene_Algebra":
        {"distrib_deps": ["HOL-Word"],
         "afp_deps": []
        }
      }, 
      {"Gauss_Jordan":
        {"distrib_deps": ["HOL-Analysis"],
         "afp_deps": ["Rank_Nullity_Theorem"]
        }
      }, 
      {"Minsky_Machines":
        {"distrib_deps": [],
         "afp_deps": ["Abstract-Rewriting", "Recursion-Theory-I"]
        }
      }, 
      {"ShortestPath":
        {"distrib_deps": [],
         "afp_deps": ["Graph_Theory"]
        }
      }, 
      {"Types_Tableaus_and_Goedels_God":
        {"distrib_deps": ["HOL"],
         "afp_deps": []
        }
      }, 
      {"Architectural_Design_Patterns":
        {"distrib_deps": [],
         "afp_deps": ["DynamicArchitectures"]
        }
      }, 
      {"FeatherweightJava":
        {"distrib_deps": ["HOL"],
         "afp_deps": []
        }
      }, 
      {"Dirichlet_Series":
        {"distrib_deps": ["HOL-Analysis", "HOL-Computational_Algebra", "HOL-Number_Theory", "HOL-Real_Asymp"],
         "afp_deps": ["Euler_MacLaurin", "Landau_Symbols", "Polynomial_Factorization"]
        }
      }, 
      {"Huffman":
        {"distrib_deps": ["HOL"],
         "afp_deps": []
        }
      }, 
      {"FinFun":
        {"distrib_deps": ["HOL", "HOL-Library"],
         "afp_deps": []
        }
      }, 
      {"Relation_Algebra":
        {"distrib_deps": [],
         "afp_deps": ["Kleene_Algebra"]
        }
      }, 
      {"Abstract_Completeness":
        {"distrib_deps": ["HOL-Library"],
         "afp_deps": ["Collections"]
        }
      }, 
      {"Tree_Decomposition":
        {"distrib_deps": ["HOL"],
         "afp_deps": []
        }
      }, 
      {"Network_Security_Policy_Verification":
        {"distrib_deps": ["HOL", "HOL-Lattice", "HOL-Library"],
         "afp_deps": ["Automatic_Refinement", "Transitive-Closure"]
        }
      }, 
      {"Random_BSTs":
        {"distrib_deps": ["HOL-Data_Structures"],
         "afp_deps": ["Landau_Symbols", "Quick_Sort_Cost"]
        }
      }, 
      {"WebAssembly":
        {"distrib_deps": ["HOL-Library"],
         "afp_deps": ["Native_Word"]
        }
      }, 
      {"DiscretePricing":
        {"distrib_deps": ["HOL-Probability"],
         "afp_deps": []
        }
      }, 
      {"SequentInvertibility":
        {"distrib_deps": ["HOL-Nominal"],
         "afp_deps": []
        }
      }, 
      {"Diophantine_Eqns_Lin_Hom":
        {"distrib_deps": ["HOL"],
         "afp_deps": []
        }
      }, 
      {"CRDT":
        {"distrib_deps": ["HOL", "HOL-Library"],
         "afp_deps": []
        }
      }, 
      {"Imperative_Insertion_Sort":
        {"distrib_deps": ["HOL-Imperative_HOL"],
         "afp_deps": []
        }
      }, 
      {"Hermite":
        {"distrib_deps": [],
         "afp_deps": ["Echelon_Form"]
        }
      }, 
      {"Bertrands_Postulate":
        {"distrib_deps": ["HOL-Decision_Procs", "HOL-Number_Theory"],
         "afp_deps": ["Pratt_Certificate"]
        }
      }, 
      {"EdmondsKarp_Maxflow":
        {"distrib_deps": [],
         "afp_deps": ["Flow_Networks"]
        }
      }, 
      {"First_Welfare_Theorem":
        {"distrib_deps": ["HOL-Analysis"],
         "afp_deps": []
        }
      }, 
      {"Probabilistic_Prime_Tests":
        {"distrib_deps": ["HOL-Algebra", "HOL-Computational_Algebra", "HOL-Number_Theory", "HOL-Probability"],
         "afp_deps": []
        }
      }, 
      {"Lambda_Free_KBOs":
        {"distrib_deps": ["HOL-Cardinals"],
         "afp_deps": ["Lambda_Free_RPOs", "Nested_Multisets_Ordinals", "Polynomials", "Regular-Sets"]
        }
      }, 
      {"DiskPaxos":
        {"distrib_deps": ["HOL"],
         "afp_deps": []
        }
      }, 
      {"Card_Multisets":
        {"distrib_deps": ["HOL", "HOL-Library"],
         "afp_deps": []
        }
      }, 
      {"Source_Coding_Theorem":
        {"distrib_deps": ["HOL-Probability"],
         "afp_deps": []
        }
      }, 
      {"Partial_Function_MR":
        {"distrib_deps": ["HOL", "HOL-Library"],
         "afp_deps": []
        }
      }, 
      {"Binomial-Queues":
        {"distrib_deps": ["HOL"],
         "afp_deps": []
        }
      }, 
      {"Density_Compiler":
        {"distrib_deps": ["HOL-Probability"],
         "afp_deps": []
        }
      }, 
      {"Gauss-Jordan-Elim-Fun":
        {"distrib_deps": ["HOL"],
         "afp_deps": []
        }
      }, 
      {"MiniML":
        {"distrib_deps": ["HOL"],
         "afp_deps": []
        }
      }, 
      {"Valuation":
        {"distrib_deps": [],
         "afp_deps": ["Group-Ring-Module"]
        }
      }, 
      {"InformationFlowSlicing":
        {"distrib_deps": [],
         "afp_deps": ["Slicing"]
        }
      }, 
      {"Affine_Arithmetic":
        {"distrib_deps": ["HOL-Analysis", "HOL-Decision_Procs"],
         "afp_deps": ["Deriving", "List-Index", "Show"]
        }
      }, 
      {"Chord_Segments":
        {"distrib_deps": ["HOL-Analysis"],
         "afp_deps": ["Triangle"]
        }
      }, 
      {"Residuated_Lattices":
        {"distrib_deps": [],
         "afp_deps": ["Relation_Algebra"]
        }
      }, 
      {"Locally-Nameless-Sigma":
        {"distrib_deps": ["HOL"],
         "afp_deps": ["Applicative_Lifting"]
        }
      }, 
      {"Pairing_Heap":
        {"distrib_deps": ["HOL-Data_Structures", "HOL-Library"],
         "afp_deps": []
        }
      }, 
      {"List_Inversions":
        {"distrib_deps": ["HOL", "HOL-Library"],
         "afp_deps": []
        }
      }, 
      {"Key_Agreement_Strong_Adversaries":
        {"distrib_deps": ["HOL"],
         "afp_deps": []
        }
      }, 
      {"Perfect-Number-Thm":
        {"distrib_deps": ["HOL-Algebra"],
         "afp_deps": []
        }
      }, 
      {"Stewart_Apollonius":
        {"distrib_deps": ["HOL-Analysis"],
         "afp_deps": ["Triangle"]
        }
      }, 
      {"Matrix_Tensor":
        {"distrib_deps": [],
         "afp_deps": ["Matrix"]
        }
      }, 
      {"Ramsey-Infinite":
        {"distrib_deps": ["HOL", "HOL-Library"],
         "afp_deps": []
        }
      }, 
      {"Circus":
        {"distrib_deps": ["HOLCF"],
         "afp_deps": []
        }
      }, 
      {"Topology":
        {"distrib_deps": [],
         "afp_deps": ["Coinductive", "Lazy-Lists-II"]
        }
      }, 
      {"Iptables_Semantics":
        {"distrib_deps": [],
         "afp_deps": ["Native_Word", "Routing"]
        }
      }, 
      {"Shivers-CFA":
        {"distrib_deps": ["HOLCF"],
         "afp_deps": []
        }
      }, 
      {"Psi_Calculi":
        {"distrib_deps": ["HOL-Nominal"],
         "afp_deps": []
        }
      }, 
      {"Monomorphic_Monad":
        {"distrib_deps": ["HOL-Probability"],
         "afp_deps": []
        }
      }, 
      {"Marriage":
        {"distrib_deps": ["HOL"],
         "afp_deps": []
        }
      }, 
      {"Stable_Matching":
        {"distrib_deps": ["HOL-Library"],
         "afp_deps": []
        }
      }, 
      {"Noninterference_Concurrent_Composition":
        {"distrib_deps": [],
         "afp_deps": ["Noninterference_Sequential_Composition"]
        }
      }, 
      {"Separata":
        {"distrib_deps": ["HOL-Eisbach", "HOL-Library"],
         "afp_deps": ["Separation_Algebra"]
        }
      }, 
      {"Knot_Theory":
        {"distrib_deps": [],
         "afp_deps": ["Matrix_Tensor"]
        }
      }, 
      {"Ptolemys_Theorem":
        {"distrib_deps": ["HOL-Analysis"],
         "afp_deps": []
        }
      }, 
      {"Myhill-Nerode":
        {"distrib_deps": ["HOL-Library"],
         "afp_deps": ["Abstract-Rewriting", "Open_Induction", "Regular-Sets", "Well_Quasi_Orders"]
        }
      }, 
      {"Stone_Kleene_Relation_Algebras":
        {"distrib_deps": [],
         "afp_deps": ["Stone_Relation_Algebras"]
        }
      }, 
      {"Optimal_BST":
        {"distrib_deps": ["HOL-Imperative_HOL", "HOL-Library"],
         "afp_deps": ["Monad_Memo_DP"]
        }
      }, 
      {"Stream_Fusion_Code":
        {"distrib_deps": [],
         "afp_deps": ["Coinductive"]
        }
      }, 
      {"Selection_Heap_Sort":
        {"distrib_deps": ["HOL-Library"],
         "afp_deps": []
        }
      }, 
      {"Differential_Dynamic_Logic":
        {"distrib_deps": [],
         "afp_deps": ["Ordinary_Differential_Equations"]
        }
      }, 
      {"Kuratowski_Closure_Complement":
        {"distrib_deps": ["HOL-Analysis"],
         "afp_deps": []
        }
      }, 
      {"XML":
        {"distrib_deps": ["HOL-Library"],
         "afp_deps": ["Certification_Monads", "Show"]
        }
      }, 
      {"Quantales":
        {"distrib_deps": [],
         "afp_deps": ["Kleene_Algebra", "Order_Lattice_Props"]
        }
      }, 
      {"Dict_Construction":
        {"distrib_deps": ["HOL", "HOL-Library"],
         "afp_deps": ["Automatic_Refinement", "Lazy_Case", "Show"]
        }
      }, 
      {"Game_Based_Crypto":
        {"distrib_deps": [],
         "afp_deps": ["CryptHOL"]
        }
      }, 
      {"Rank_Nullity_Theorem":
        {"distrib_deps": ["HOL-Analysis"],
         "afp_deps": []
        }
      }, 
      {"Incompleteness":
        {"distrib_deps": [],
         "afp_deps": ["HereditarilyFinite", "Nominal2"]
        }
      }, 
      {"Buffons_Needle":
        {"distrib_deps": ["HOL-Probability"],
         "afp_deps": []
        }
      }, 
      {"Possibilistic_Noninterference":
        {"distrib_deps": ["HOL"],
         "afp_deps": []
        }
      }, 
      {"Multirelations":
        {"distrib_deps": [],
         "afp_deps": ["Kleene_Algebra"]
        }
      }, 
      {"KBPs":
        {"distrib_deps": ["HOL-Library"],
         "afp_deps": ["Transitive-Closure", "Trie"]
        }
      }, 
      {"Concurrent_Ref_Alg":
        {"distrib_deps": ["HOL", "HOL-Library"],
         "afp_deps": []
        }
      }, 
      {"Irrationality_J_Hancl":
        {"distrib_deps": ["HOL-Analysis", "HOL-Decision_Procs"],
         "afp_deps": []
        }
      }, 
      {"PSemigroupsConvolution":
        {"distrib_deps": ["HOL"],
         "afp_deps": []
        }
      }, 
      {"AODV":
        {"distrib_deps": [],
         "afp_deps": ["AWN"]
        }
      }, 
      {"pGCL":
        {"distrib_deps": ["HOL-Analysis"],
         "afp_deps": []
        }
      }, 
      {"Graph_Saturation":
        {"distrib_deps": ["HOL-Library"],
         "afp_deps": []
        }
      }, 
      {"Count_Complex_Roots":
        {"distrib_deps": ["HOL-Analysis"],
         "afp_deps": ["Sturm_Tarski", "Winding_Number_Eval"]
        }
      }, 
      {"Secondary_Sylow":
        {"distrib_deps": ["HOL-Algebra"],
         "afp_deps": []
        }
      }, 
      {"Transitive-Closure":
        {"distrib_deps": [],
         "afp_deps": ["Collections", "Matrix"]
        }
      }, 
      {"Special_Function_Bounds":
        {"distrib_deps": [],
         "afp_deps": ["Sturm_Sequences"]
        }
      }, 
      {"Boolean_Expression_Checkers":
        {"distrib_deps": ["HOL-Library"],
         "afp_deps": []
        }
      }, 
      {"Strong_Security":
        {"distrib_deps": ["HOL"],
         "afp_deps": []
        }
      }, 
      {"Smooth_Manifolds":
        {"distrib_deps": ["HOL-Analysis", "HOL-Library", "HOL-Types_To_Sets"],
         "afp_deps": []
        }
      }, 
      {"Lam-ml-Normalization":
        {"distrib_deps": ["HOL-Nominal"],
         "afp_deps": []
        }
      }, 
      {"QR_Decomposition":
        {"distrib_deps": ["HOL-Analysis"],
         "afp_deps": ["Gauss_Jordan", "Rank_Nullity_Theorem", "Real_Impl", "Sqrt_Babylonian"]
        }
      }, 
      {"Refine_Monadic":
        {"distrib_deps": ["HOL-Word"],
         "afp_deps": ["Automatic_Refinement"]
        }
      }, 
      {"Perron_Frobenius":
        {"distrib_deps": ["HOL-Types_To_Sets"],
         "afp_deps": ["Jordan_Normal_Form", "Polynomial_Factorization", "Rank_Nullity_Theorem", "Sturm_Sequences"]
        }
      }, 
      {"List_Interleaving":
        {"distrib_deps": ["HOL"],
         "afp_deps": []
        }
      }, 
      {"AVL-Trees":
        {"distrib_deps": ["HOL"],
         "afp_deps": []
        }
      }, 
      {"Factored_Transition_System_Bounding":
        {"distrib_deps": ["HOL", "HOL-Library"],
         "afp_deps": []
        }
      }, 
      {"FOL-Fitting":
        {"distrib_deps": ["HOL-Library"],
         "afp_deps": []
        }
      }, 
      {"Hidden_Markov_Models":
        {"distrib_deps": ["HOL-Library"],
         "afp_deps": ["Markov_Models", "Monad_Memo_DP"]
        }
      }, 
      {"MonoBoolTranAlgebra":
        {"distrib_deps": ["HOL"],
         "afp_deps": ["LatticeProperties"]
        }
      }, 
      {"Posix-Lexing":
        {"distrib_deps": [],
         "afp_deps": ["Regular-Sets"]
        }
      }, 
      {"HyperCTL":
        {"distrib_deps": ["HOL-Library"],
         "afp_deps": []
        }
      }, 
      {"Falling_Factorial_Sum":
        {"distrib_deps": ["HOL-Library"],
         "afp_deps": ["Card_Partitions", "Discrete_Summation"]
        }
      }, 
      {"Modular_Assembly_Kit_Security":
        {"distrib_deps": ["HOL"],
         "afp_deps": []
        }
      }, 
      {"Flyspeck-Tame":
        {"distrib_deps": ["HOL", "HOL-Library"],
         "afp_deps": ["Trie"]
        }
      }, 
      {"Green":
        {"distrib_deps": ["HOL-Analysis"],
         "afp_deps": []
        }
      }, 
      {"Automatic_Refinement":
        {"distrib_deps": ["HOL", "HOL-Eisbach", "HOL-Library", "HOL-ex"],
         "afp_deps": []
        }
      }, 
      {"ClockSynchInst":
        {"distrib_deps": ["HOL"],
         "afp_deps": []
        }
      }, 
      {"Pratt_Certificate":
        {"distrib_deps": ["HOL-Number_Theory"],
         "afp_deps": ["Lehmer"]
        }
      }, 
      {"Elliptic_Curves_Group_Law":
        {"distrib_deps": ["HOL-Decision_Procs", "HOL-Number_Theory"],
         "afp_deps": []
        }
      }, 
      {"Core_DOM":
        {"distrib_deps": ["HOL-Library"],
         "afp_deps": []
        }
      }, 
      {"Free-Boolean-Algebra":
        {"distrib_deps": ["HOL"],
         "afp_deps": []
        }
      }, 
      {"Groebner_Bases":
        {"distrib_deps": ["HOL-Algebra"],
         "afp_deps": ["Deriving", "Jordan_Normal_Form", "Polynomials"]
        }
      }, 
      {"VolpanoSmith":
        {"distrib_deps": ["HOL"],
         "afp_deps": []
        }
      }, 
      {"SenSocialChoice":
        {"distrib_deps": ["HOL"],
         "afp_deps": []
        }
      }, 
      {"LightweightJava":
        {"distrib_deps": ["HOL-Library"],
         "afp_deps": []
        }
      }, 
      {"IMP2":
        {"distrib_deps": ["HOL", "HOL-Eisbach", "HOL-Library"],
         "afp_deps": []
        }
      }, 
      {"Completeness":
        {"distrib_deps": ["HOL", "HOL-Library"],
         "afp_deps": []
        }
      }, 
      {"Tycon":
        {"distrib_deps": ["HOLCF"],
         "afp_deps": []
        }
      }, 
      {"FOL_Harrison":
        {"distrib_deps": ["HOL", "HOL-Library"],
         "afp_deps": []
        }
      }, 
      {"Optics":
        {"distrib_deps": ["HOL-Eisbach", "HOL-Library"],
         "afp_deps": []
        }
      }, 
      {"Regular_Algebras":
        {"distrib_deps": [],
         "afp_deps": ["Kleene_Algebra"]
        }
      }, 
      {"Concurrent_Revisions":
        {"distrib_deps": ["HOL"],
         "afp_deps": []
        }
      }, 
      {"Impossible_Geometry":
        {"distrib_deps": ["HOL"],
         "afp_deps": []
        }
      }, 
      {"Lp":
        {"distrib_deps": ["HOL-Probability"],
         "afp_deps": ["Ergodic_Theory"]
        }
      }, 
      {"Call_Arity":
        {"distrib_deps": [],
         "afp_deps": ["Launchbury"]
        }
      }, 
      {"Probabilistic_While":
        {"distrib_deps": ["HOL-Probability"],
         "afp_deps": ["MFMC_Countable", "Berlekamp_Zassenhaus"]
        }
      }, 
      {"Catalan_Numbers":
        {"distrib_deps": ["HOL-Analysis"],
         "afp_deps": ["Landau_Symbols"]
        }
      }, 
      {"E_Transcendental":
        {"distrib_deps": ["HOL-Analysis", "HOL-Number_Theory"],
         "afp_deps": []
        }
      }, 
      {"Slicing":
        {"distrib_deps": [],
         "afp_deps": ["Jinja"]
        }
      }, 
      {"Skew_Heap":
        {"distrib_deps": ["HOL-Data_Structures", "HOL-Library"],
         "afp_deps": []
        }
      }, 
      {"Order_Lattice_Props":
        {"distrib_deps": ["HOL-Library"],
         "afp_deps": []
        }
      }, 
      {"Constructor_Funs":
        {"distrib_deps": ["HOL"],
         "afp_deps": []
        }
      }, 
      {"RIPEMD-160-SPARK":
        {"distrib_deps": ["HOL-SPARK-Examples"],
         "afp_deps": []
        }
      }, 
      {"LOFT":
        {"distrib_deps": [],
         "afp_deps": ["Iptables_Semantics"]
        }
      }, 
      {"Dependent_SIFUM_Type_Systems":
        {"distrib_deps": ["HOL", "HOL-Eisbach"],
         "afp_deps": []
        }
      }, 
      {"Presburger-Automata":
        {"distrib_deps": ["HOL-Library"],
         "afp_deps": []
        }
      }, 
      {"BytecodeLogicJmlTypes":
        {"distrib_deps": ["HOL"],
         "afp_deps": []
        }
      }, 
      {"Security_Protocol_Refinement":
        {"distrib_deps": ["HOL"],
         "afp_deps": []
        }
      }, 
      {"FFT":
        {"distrib_deps": ["HOL"],
         "afp_deps": []
        }
      }, 
      {"Buchi_Complementation":
        {"distrib_deps": [],
         "afp_deps": ["Transition_Systems_and_Automata"]
        }
      }, 
      {"Nominal2":
        {"distrib_deps": ["HOL", "HOL-Library"],
         "afp_deps": ["FinFun"]
        }
      }, 
      {"Projective_Geometry":
        {"distrib_deps": ["HOL"],
         "afp_deps": []
        }
      }, 
      {"Applicative_Lifting":
        {"distrib_deps": ["HOL-Nonstandard_Analysis", "HOL-Probability", "HOL-Proofs-Lambda"],
         "afp_deps": []
        }
      }, 
      {"Pi_Transcendental":
        {"distrib_deps": ["HOL-Computational_Algebra", "HOL-Real_Asymp"],
         "afp_deps": ["E_Transcendental", "Symmetric_Polynomials"]
        }
      }, 
      {"FunWithFunctions":
        {"distrib_deps": ["HOL"],
         "afp_deps": []
        }
      }, 
      {"MuchAdoAboutTwo":
        {"distrib_deps": ["HOL-Library"],
         "afp_deps": []
        }
      }, 
      {"Deep_Learning":
        {"distrib_deps": ["HOL-Algebra", "HOL-Probability"],
         "afp_deps": ["Jordan_Normal_Form", "Polynomial_Interpolation", "Polynomials", "VectorSpace"]
        }
      }, 
      {"UPF":
        {"distrib_deps": ["HOL"],
         "afp_deps": []
        }
      }, 
      {"Bell_Numbers_Spivey":
        {"distrib_deps": ["HOL-Library"],
         "afp_deps": ["Card_Partitions"]
        }
      }, 
      {"Max-Card-Matching":
        {"distrib_deps": ["HOL"],
         "afp_deps": []
        }
      }, 
      {"AxiomaticCategoryTheory":
        {"distrib_deps": ["HOL"],
         "afp_deps": []
        }
      }, 
      {"Kruskal":
        {"distrib_deps": [],
         "afp_deps": ["Collections", "Matroids", "Refine_Imperative_HOL", "Refine_Monadic"]
        }
      }, 
      {"Koenigsberg_Friendship":
        {"distrib_deps": ["HOL-Number_Theory"],
         "afp_deps": ["Dijkstra_Shortest_Path"]
        }
      }, 
      {"Planarity_Certificates":
        {"distrib_deps": ["HOL-Eisbach"],
         "afp_deps": ["Case_Labeling", "Graph_Theory", "List-Index", "Simpl", "Transitive-Closure"]
        }
      }, 
      {"HRB-Slicing":
        {"distrib_deps": [],
         "afp_deps": ["Jinja"]
        }
      }, 
      {"Allen_Calculus":
        {"distrib_deps": ["HOL", "HOL-Eisbach"],
         "afp_deps": []
        }
      }, 
      {"Linear_Recurrences":
        {"distrib_deps": ["HOL-Analysis", "HOL-Computational_Algebra", "HOL-Library", "HOL-Real_Asymp"],
         "afp_deps": ["Count_Complex_Roots", "Polynomial_Factorization", "Algebraic_Numbers", "Berlekamp_Zassenhaus"]
        }
      }, 
      {"Symmetric_Polynomials":
        {"distrib_deps": ["HOL-Computational_Algebra", "HOL-Library"],
         "afp_deps": ["Polynomials"]
        }
      }, 
      {"Decreasing-Diagrams-II":
        {"distrib_deps": ["HOL-Cardinals"],
         "afp_deps": ["Abstract-Rewriting", "Open_Induction", "Well_Quasi_Orders"]
        }
      }, 
      {"Featherweight_OCL":
        {"distrib_deps": ["HOL"],
         "afp_deps": []
        }
      }, 
      {"BNF_CC":
        {"distrib_deps": ["HOL", "HOL-Library"],
         "afp_deps": []
        }
      }, 
      {"Noninterference_Generic_Unwinding":
        {"distrib_deps": [],
         "afp_deps": ["Noninterference_Ipurge_Unwinding"]
        }
      }, 
      {"Budan_Fourier":
        {"distrib_deps": ["HOL-Computational_Algebra"],
         "afp_deps": ["Sturm_Tarski"]
        }
      }, 
      {"Card_Partitions":
        {"distrib_deps": ["HOL", "HOL-Eisbach"],
         "afp_deps": ["Discrete_Summation"]
        }
      }, 
      {"HotelKeyCards":
        {"distrib_deps": ["HOL", "HOL-Library"],
         "afp_deps": []
        }
      }, 
      {"Probabilistic_Timed_Automata":
        {"distrib_deps": ["HOL-Eisbach"],
         "afp_deps": ["Markov_Models", "Timed_Automata"]
        }
      }, 
      {"Randomised_BSTs":
        {"distrib_deps": [],
         "afp_deps": ["Monad_Normalisation", "Random_BSTs"]
        }
      }, 
      {"Pi_Calculus":
        {"distrib_deps": ["HOL-Nominal"],
         "afp_deps": []
        }
      }, 
      {"Zeta_Function":
        {"distrib_deps": ["HOL-Library", "HOL-Real_Asymp"],
         "afp_deps": ["Bernoulli", "Dirichlet_Series", "Euler_MacLaurin", "Winding_Number_Eval"]
        }
      }, 
      {"Incredible_Proof_Machine":
        {"distrib_deps": ["HOL-Eisbach", "HOL-Library"],
         "afp_deps": ["Abstract_Completeness"]
        }
      }, 
      {"Roy_Floyd_Warshall":
        {"distrib_deps": ["HOL"],
         "afp_deps": []
        }
      }, 
      {"JiveDataStoreModel":
        {"distrib_deps": ["HOL"],
         "afp_deps": []
        }
      }, 
      {"GoedelGod":
        {"distrib_deps": ["HOL"],
         "afp_deps": []
        }
      }, 
      {"Algebraic_VCs":
        {"distrib_deps": ["HOL-Eisbach", "HOL-Hoare"],
         "afp_deps": ["KAD", "KAT_and_DRA"]
        }
      }, 
      {"RefinementReactive":
        {"distrib_deps": ["HOL"],
         "afp_deps": []
        }
      }, 
      {"Modal_Logics_for_NTS":
        {"distrib_deps": ["HOL-Cardinals"],
         "afp_deps": ["Nominal2"]
        }
      }, 
      {"Parity_Game":
        {"distrib_deps": ["HOL", "HOL-Library"],
         "afp_deps": ["Coinductive", "Graph_Theory"]
        }
      }, 
      {"Splay_Tree":
        {"distrib_deps": ["HOL-Data_Structures", "HOL-Library"],
         "afp_deps": []
        }
      }, 
      {"ArrowImpossibilityGS":
        {"distrib_deps": ["HOL", "HOL-Library"],
         "afp_deps": []
        }
      }, 
      {"Farkas":
        {"distrib_deps": [],
         "afp_deps": ["Simplex"]
        }
      }, 
      {"Name_Carrying_Type_Inference":
        {"distrib_deps": ["HOL"],
         "afp_deps": []
        }
      }, 
      {"AnselmGod":
        {"distrib_deps": ["HOL"],
         "afp_deps": []
        }
      }, 
      {"Fishburn_Impossibility":
        {"distrib_deps": ["HOL"],
         "afp_deps": ["Randomised_Social_Choice"]
        }
      }, 
      {"CCS":
        {"distrib_deps": ["HOL-Nominal"],
         "afp_deps": []
        }
      }, 
      {"Ordinary_Differential_Equations":
        {"distrib_deps": ["HOL-Types_To_Sets", "HOL-Analysis", "HOL-Decision_Procs"],
         "afp_deps": ["Affine_Arithmetic", "Collections", "Deriving", "Show", "List-Index", "Triangle"]
        }
      }, 
      {"Ordinals_and_Cardinals":
        {"distrib_deps": ["HOL-Cardinals"],
         "afp_deps": []
        }
      }, 
      {"Auto2_HOL":
        {"distrib_deps": ["HOL", "HOL-Library"],
         "afp_deps": []
        }
      }, 
      {"FocusStreamsCaseStudies":
        {"distrib_deps": ["HOL"],
         "afp_deps": []
        }
      }, 
      {"Rewriting_Z":
        {"distrib_deps": ["HOL-Eisbach"],
         "afp_deps": ["Abstract-Rewriting", "Nominal2"]
        }
      }, 
      {"Flow_Networks":
        {"distrib_deps": [],
         "afp_deps": ["CAVA_Automata", "DFS_Framework", "Program-Conflict-Analysis", "Refine_Imperative_HOL"]
        }
      }, 
      {"Encodability_Process_Calculi":
        {"distrib_deps": ["HOL", "HOL-Library"],
         "afp_deps": []
        }
      }, 
      {"LinearQuantifierElim":
        {"distrib_deps": ["HOL-Library"],
         "afp_deps": []
        }
      }, 
      {"BNF_Operations":
        {"distrib_deps": ["HOL", "HOL-Library"],
         "afp_deps": []
        }
      }, 
      {"Polynomial_Interpolation":
        {"distrib_deps": ["HOL-Computational_Algebra"],
         "afp_deps": ["Sqrt_Babylonian"]
        }
      }, 
      {"CryptHOL":
        {"distrib_deps": ["HOL-Algebra", "HOL-Eisbach"],
         "afp_deps": ["Applicative_Lifting", "Coinductive", "Landau_Symbols", "Monad_Normalisation", "Monomorphic_Monad", "Probabilistic_While"]
        }
      }, 
      {"Probabilistic_Noninterference":
        {"distrib_deps": ["HOL-Probability"],
         "afp_deps": ["Coinductive", "Markov_Models"]
        }
      }, 
      {"Generic_Deriving":
        {"distrib_deps": ["HOL"],
         "afp_deps": []
        }
      }, 
      {"Functional_Ordered_Resolution_Prover":
        {"distrib_deps": ["HOL-Library"],
         "afp_deps": ["First_Order_Terms", "Nested_Multisets_Ordinals", "Open_Induction", "Ordered_Resolution_Prover", "Polynomial_Factorization"]
        }
      }, 
      {"MFMC_Countable":
        {"distrib_deps": ["HOL-Probability"],
         "afp_deps": ["EdmondsKarp_Maxflow"]
        }
      }, 
      {"Quick_Sort_Cost":
        {"distrib_deps": ["HOL-Probability"],
         "afp_deps": ["Comparison_Sort_Lower_Bound", "Landau_Symbols", "List-Index", "Regular-Sets"]
        }
      }, 
      {"Finite_Automata_HF":
        {"distrib_deps": ["HOL", "HOL-Library"],
         "afp_deps": ["HereditarilyFinite", "Regular-Sets"]
        }
      }, 
      {"Trie":
        {"distrib_deps": ["HOL-Library"],
         "afp_deps": []
        }
      }, 
      {"GenClock":
        {"distrib_deps": ["HOL"],
         "afp_deps": []
        }
      }, 
      {"Noninterference_Sequential_Composition":
        {"distrib_deps": ["HOL"],
         "afp_deps": ["Noninterference_Ipurge_Unwinding"]
        }
      }, 
      {"Finger-Trees":
        {"distrib_deps": ["HOL-Library"],
         "afp_deps": []
        }
      }, 
      {"SuperCalc":
        {"distrib_deps": ["HOL-Library", "HOL-ex"],
         "afp_deps": []
        }
      }, 
      {"Landau_Symbols":
        {"distrib_deps": ["HOL-Library"],
         "afp_deps": []
        }
      }, 
      {"Transitive-Closure-II":
        {"distrib_deps": ["HOL", "HOL-Library"],
         "afp_deps": ["Regular-Sets"]
        }
      }, 
      {"AutoFocus-Stream":
        {"distrib_deps": [],
         "afp_deps": ["Nat-Interval-Logic"]
        }
      }, 
      {"Coinductive_Languages":
        {"distrib_deps": ["HOL", "HOL-Library"],
         "afp_deps": ["Regular-Sets"]
        }
      }, 
      {"Latin_Square":
        {"distrib_deps": ["HOL"],
         "afp_deps": ["Marriage"]
        }
      }, 
      {"Ordinal":
        {"distrib_deps": ["HOL"],
         "afp_deps": []
        }
      }, 
      {"Epistemic_Logic":
        {"distrib_deps": ["HOL-Library"],
         "afp_deps": []
        }
      }, 
      {"Polynomials":
        {"distrib_deps": [],
         "afp_deps": ["Abstract-Rewriting", "Matrix", "Show", "Well_Quasi_Orders"]
        }
      }, 
      {"CofGroups":
        {"distrib_deps": ["HOL", "HOL-Library"],
         "afp_deps": []
        }
      }, 
      {"Transition_Systems_and_Automata":
        {"distrib_deps": [],
         "afp_deps": ["Collections", "DFS_Framework", "Gabow_SCC"]
        }
      }, 
      {"SATSolverVerification":
        {"distrib_deps": ["HOL-Library"],
         "afp_deps": []
        }
      }, 
      {"Buildings":
        {"distrib_deps": ["HOL-Library"],
         "afp_deps": []
        }
      }, 
      {"RSAPSS":
        {"distrib_deps": ["HOL-Number_Theory"],
         "afp_deps": []
        }
      }, 
      {"Propositional_Proof_Systems":
        {"distrib_deps": ["HOL", "HOL-Library"],
         "afp_deps": []
        }
      }, 
      {"Promela":
        {"distrib_deps": [],
         "afp_deps": ["CAVA_Automata", "LTL"]
        }
      }]