Summary
- use set-based lifting for single-variable invariants
The file was modified | thys/Stern_Brocot/Cotree.thy (diff) |
The file was modified | thys/Stern_Brocot/Stern_Brocot_Tree.thy (diff) |
The file was modified | thys/Stern_Brocot/Cotree.thy (diff) |
The file was modified | thys/Stern_Brocot/Stern_Brocot_Tree.thy (diff) |