Session Transition_Systems_and_Automata

Theories

• Basic
• HOL-Library.Nat_Bijection
• HOL-Library.Stream
• Sequence
• HOL-Library.Sublist
• HOL-Library.Old_Datatype
  • File ‹~~/src/HOL/Tools/Old_Datatype/old_datatype.ML›
• 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.Linear_Temporal_Logic_on_Streams
• Sequence_LTL
• Sequence_Zip
• Maps
• Acceptance
• Degeneralization
• Transition_System
• Transition_System_Extra
• Transition_System_Construction
• Deterministic
• DFA
• Nondeterministic
• NFA
• DBA
• DGBA
• DBA_Combine
• DBTA
• DGBTA
• DBTA_Combine
• DCA
• DGCA
• DCA_Combine
• DRA
• DRA_Combine
• CAVA_Base.Statistics
• CAVA_Base.Code_String
• CAVA_Base.CAVA_Code_Target
• CAVA_Base.CAVA_Base
• HOL-Library.Omega_Words_Fun
• CAVA_Automata.Digraph_Basic
• CAVA_Automata.Digraph
• DFS_Framework.DFS_Framework_Misc
• DFS_Framework.DFS_Framework_Refine_Aux
• DFS_Framework.Param_DFS
• DFS_Framework.DFS_Invars_Basic
• DFS_Framework.General_DFS_Structure
• DFS_Framework.Tailrec_Impl
• DFS_Framework.Rec_Impl
• DFS_Framework.Simple_Impl
• DFS_Framework.Restr_Impl
• DFS_Framework.DFS_Framework
• CAVA_Automata.Digraph_Impl
• DFS_Framework.Impl_Rev_Array_Stack
• DFS_Framework.Reachable_Nodes
• Refine
• Acceptance_Refine
• Transition_System_Refine
• DRA_Refine
• Implement
• DRA_Implement
• DRA_Nodes
• DRA_Explicit
• DRA_Translate
• NBA
• NGBA
• NBA_Combine
• CAVA_Automata.Automata
• CAVA_Automata.Automata_Impl
• NBA_Graphs
• NBA_Refine
• NBA_Implement
• Gabow_SCC.Gabow_Skeleton
• CAVA_Automata.Lasso
• Gabow_SCC.Find_Path
• Gabow_SCC.Gabow_GBG
• Gabow_SCC.Gabow_Skeleton_Code
• Gabow_SCC.Find_Path_Impl
• Gabow_SCC.Gabow_GBG_Code
• NBA_Algorithms
• NBA_Explicit
• NBA_Translate
• NGBA_Graphs
• NGBA_Refine
• NGBA_Implement
• Degeneralization_Refine
• NGBA_Algorithms
• NBTA
• NGBTA
• NBTA_Combine