Fixed up some more sorries. Deleted Example.thy