Summary
- merge
- added applicative KBO definition
- renamed thy + tuned wording
The file was added | thys/Lambda_Free_KBOs/Lambda_Free_KBO_App.thy |
The file was modified | thys/Lambda_Free_KBOs/Lambda_Free_KBO_Basic.thy (diff) |
The file was modified | thys/Lambda_Free_KBOs/Lambda_Free_KBO_Std.thy (diff) |
The file was modified | thys/Lambda_Free_KBOs/Lambda_Free_KBO_Util.thy (diff) |
The file was modified | thys/Lambda_Free_KBOs/Lambda_Free_KBOs.thy (diff) |
The file was added | thys/Lambda_Free_RPOs/Lambda_Free_RPO_Std.thy |
The file was modified | thys/Lambda_Free_RPOs/Lambda_Free_RPO_Optim.thy (diff) |
The file was removed | thys/Lambda_Free_RPOs/Lambda_Free_RPO_New.thy |