Session Parity_Game

Theories

• HOL-Library.Infinite_Set
• HOL-Library.Sublist
• HOL-Library.Case_Converter
  • File ‹case_converter.ML›
• HOL-Library.Simps_Case_Conv
  • File ‹simps_case_conv.ML›
• HOL-Library.Old_Datatype
  • File ‹~~/src/HOL/Tools/Old_Datatype/old_datatype.ML›
• HOL-Library.Nat_Bijection
• HOL-Library.Countable
  • File ‹~~/src/HOL/Tools/BNF/bnf_lfp_countable.ML›
• HOL-Library.Countable_Set
• HOL-Library.Countable_Complete_Lattices
• HOL-Library.Order_Continuity
• HOL-Library.Extended_Nat
• HOL-Library.Complete_Partial_Order2
• Coinductive.Coinductive_Nat
• Coinductive.Coinductive_List
• MoreCoinductiveList
• ParityGame
• Strategy
• AttractingStrategy
• Attractor
• WinningStrategy
• WellOrderedStrategy
• WinningRegion
• UniformStrategy
• AttractorStrategy
• PositionalDeterminacy
• AttractorInductive
• Graph_Theory.Rtrancl_On
• HOL-Library.Liminf_Limsup
• HOL-Library.Extended_Real
• Graph_Theory.Stuff
• Graph_Theory.Digraph
• Graph_Theory.Arc_Walk
• HOL-Library.Cancellation
  • File ‹Cancellation/cancel.ML›
  • File ‹Cancellation/cancel_data.ML›
  • File ‹Cancellation/cancel_simprocs.ML›
• HOL-Library.Multiset
  • File ‹multiset_simprocs.ML›
• HOL-Library.FuncSet
• HOL-Library.Disjoint_Sets
• HOL-Combinatorics.Transposition
• HOL-Combinatorics.Permutations
• Graph_Theory.Bidirected_Digraph
• Graph_Theory.Pair_Digraph
• Graph_Theory.Digraph_Component
• Graph_Theory.Digraph_Isomorphism
• Graph_TheoryCompatibility