--- a/src/HOL/Bali/Eval.thy Thu Sep 22 23:55:42 2005 +0200 +++ b/src/HOL/Bali/Eval.thy Thu Sep 22 23:56:15 2005 +0200 @@ -192,7 +192,7 @@ defer apply (case_tac "a' = Null") apply simp_all -apply rules +apply iprover done constdefs