--- a/src/HOL/Bali/Eval.thy Sat Jun 17 15:41:19 2017 +0200 +++ b/src/HOL/Bali/Eval.thy Sat Jun 17 18:49:19 2017 +0200 @@ -191,7 +191,6 @@ defer apply (case_tac "a' = Null") apply simp_all -apply iprover done definition