# HG changeset patch
# User nipkow
# Date 1389169214 -3600
# Node ID 9a52ee8cae9bc791356504e1817339c39fde56a8
# Parent  1276861f272437681907f5879ff3b4d7b25f0c62
tuned

diff -r 1276861f2724 -r 9a52ee8cae9b src/HOL/IMP/Abs_Int0.thy
--- a/src/HOL/IMP/Abs_Int0.thy	Tue Jan 07 23:55:51 2014 +0100
+++ b/src/HOL/IMP/Abs_Int0.thy	Wed Jan 08 09:20:14 2014 +0100
@@ -219,8 +219,7 @@
 lemma gamma_Step_subcomm:
   assumes "!!x e S. f1 x e (\<gamma>\<^sub>o S) \<subseteq> \<gamma>\<^sub>o (f2 x e S)"  "!!b S. g1 b (\<gamma>\<^sub>o S) \<subseteq> \<gamma>\<^sub>o (g2 b S)"
   shows "Step f1 g1 (\<gamma>\<^sub>o S) (\<gamma>\<^sub>c C) \<le> \<gamma>\<^sub>c (Step f2 g2 S C)"
-proof(induction C arbitrary: S)
-qed  (auto simp: mono_gamma_o assms)
+by (induction C arbitrary: S) (auto simp: mono_gamma_o assms)
 
 lemma step_step': "step (\<gamma>\<^sub>o S) (\<gamma>\<^sub>c C) \<le> \<gamma>\<^sub>c (step' S C)"
 unfolding step_def step'_def