Session Lambda_Free_RPOs

View theory dependencies
View document
View outline

Theories

Lambda_Free_Util
Lambda_Free_Term
Infinite_Chain
HOL-Cardinals.Order_Union
HOL-Cardinals.Wellorder_Extension
Extension_Orders
Lambda_Free_RPO_App
Nested_Multisets_Ordinals.Multiset_More
Lambda_Free_RPO_Std
Lambda_Free_RPO_Optim
Lambda_Encoding
Lambda_Free_RPOs