Christine Rizkallah

Is it easy to merge this branch with master? Subtyping.thy has some proofs about evaluation being deterministic that would be good to have.