Diffusion afp-devel 8c71faeab7b8

Optimal_BST: simplify termination proofs
8c71faeab7b8
Actions

Tags

None

Subscribers

None

Description

Optimal_BST: simplify termination proofs

Details

Provenance

Simon Wimmer <wimmers@in.tum.de>

Authored on

Parents

rAFP9cebf89c45f7: Monad_Memo_DP: clean proof, remove unused thms, clean tests

Branches

Unknown

Tags

Unknown

Event Timeline

Simon Wimmer <wimmers@in.tum.de> committed rAFP8c71faeab7b8: Optimal_BST: simplify termination proofs.Jan 20 2021, 3:43 PM

Changes (1)

Path

Size

thys/

Optimal_BST/

Optimal_BST2.thy

rAFP8c71faeab7b8

thys/Optimal_BST/Optimal_BST2.thy

Loading...