--- a/src/HOL/IMP/Def_Init_Small.thy Fri Jul 22 08:02:37 2016 +0200
+++ b/src/HOL/IMP/Def_Init_Small.thy Fri Jul 22 11:00:43 2016 +0200
@@ -58,10 +58,9 @@
"(c,s) \<rightarrow> (c',s') \<Longrightarrow> D (dom s) c A \<Longrightarrow> EX A'. D (dom s') c' A' & A <= A'"
proof (induction arbitrary: A rule: small_step_induct)
case (While b c s)
- then obtain A' where "vars b \<subseteq> dom s" "A = dom s" "D (dom s) c A'" by blast
- moreover
+ then obtain A' where A': "vars b \<subseteq> dom s" "A = dom s" "D (dom s) c A'" by blast
then obtain A'' where "D A' c A''" by (metis D_incr D_mono)
- ultimately have "D (dom s) (IF b THEN c;; WHILE b DO c ELSE SKIP) (dom s)"
+ with A' have "D (dom s) (IF b THEN c;; WHILE b DO c ELSE SKIP) (dom s)"
by (metis D.If[OF `vars b \<subseteq> dom s` D.Seq[OF `D (dom s) c A'` D.While[OF _ `D A' c A''`]] D.Skip] D_incr Int_absorb1 subset_trans)
thus ?case by (metis D_incr `A = dom s`)
next