--- a/src/HOL/NanoJava/Example.thy Tue Aug 09 23:29:54 2016 +0200
+++ b/src/HOL/NanoJava/Example.thy Wed Aug 10 09:33:54 2016 +0200
@@ -184,7 +184,7 @@
apply rule
apply (rule hoare_ehoare.Asm) (* 20 *)
apply (rule_tac a = "((case n of 0 \<Rightarrow> 0 | Suc m \<Rightarrow> m),m+1)" in UN_I, rule+)
-apply (clarsimp split add: nat.split_asm dest!: Nat_atleast_mono)
+apply (clarsimp split: nat.split_asm dest!: Nat_atleast_mono)
apply rule
apply (rule hoare_ehoare.Call) (* 21 *)
apply (rule hoare_ehoare.LAcc)