Finish updating Exp.thy.
Use observation functions instead of Ord instances.