Session MSO_Regex_Equivalence
View
theory dependencies
View
document
View
outline
Theories
List-Index.List_Index
HOL-Library.Cancellation
File ‹Cancellation/cancel.ML›
File ‹Cancellation/cancel_data.ML›
File ‹Cancellation/cancel_simprocs.ML›
HOL-Library.Multiset
File ‹multiset_simprocs.ML›
List_More
Pi_Regular_Set
HOL-Library.List_Lexorder
HOL-Library.Code_Abstract_Nat
HOL-Library.Code_Target_Nat
Deriving.Generator_Aux
File ‹bnf_access.ML›
File ‹generator_aux.ML›
Deriving.Derive_Manager
File ‹derive_manager.ML›
Deriving.Comparator
Deriving.Comparator_Generator
File ‹comparator_generator.ML›
Deriving.Compare
File ‹compare_code.ML›
Deriving.Compare_Generator
File ‹compare_generator.ML›
HOL-Library.Char_ord
Deriving.Compare_Instances
Pi_Regular_Exp
Pi_Derivatives
HOL-Library.While_Combinator
Pi_Regular_Operators
Pi_Regular_Exp_Dual
Pi_Equivalence_Checking
HOL-Library.Case_Converter
File ‹case_converter.ML›
HOL-Library.Simps_Case_Conv
File ‹simps_case_conv.ML›
Init_Normalization
PNormalization
Formula
M2L
M2L_Normalization
M2L_Equivalence_Checking
HOL-Library.Nat_Bijection
HOL-Library.Stream
WS1S
WS1S_Normalization
WS1S_Equivalence_Checking
HOL-Library.Product_Lexorder
M2L_Examples
WS1S_Examples