Session Lambda_Free_KBOs
View
theory dependencies
View
document
View
outline
Theories
Lambda_Free_RPOs.Lambda_Free_Util
Lambda_Free_RPOs.Lambda_Free_Term
Lambda_Free_RPOs.Infinite_Chain
HOL-Cardinals.Order_Union
HOL-Cardinals.Wellorder_Extension
Lambda_Free_RPOs.Extension_Orders
Regular-Sets.Regular_Set
Regular-Sets.Regular_Exp
Regular-Sets.NDerivative
HOL-Library.While_Combinator
Regular-Sets.Equivalence_Checking
Regular-Sets.Relation_Interpretation
Regular-Sets.Regexp_Method
Abstract-Rewriting.Seq
Abstract-Rewriting.Abstract_Rewriting
Abstract-Rewriting.SN_Orders
Matrix.Utility
Polynomials.Polynomials
Lambda_Free_KBO_Util
Lambda_Free_KBO_App
Lambda_Free_KBO_Std
Lambda_Free_KBO_Basic
Lambda_Free_TKBO_Coefs
Lambda_Free_RPOs.Lambda_Encoding
Lambda_Encoding_KBO
Lambda_Free_KBOs