# HG changeset patch
# User nipkow
# Date 1365685822 -7200
# Node ID 6ae88642962f5e229a041059c46b57e31dc41a6e
# Parent  1eb533ea148059a711bc0ae59cef7c19ce2040f1
tuned

diff -r 1eb533ea1480 -r 6ae88642962f src/HOL/IMP/Abs_Int0.thy
--- a/src/HOL/IMP/Abs_Int0.thy	Wed Apr 10 21:46:28 2013 +0200
+++ b/src/HOL/IMP/Abs_Int0.thy	Thu Apr 11 15:10:22 2013 +0200
@@ -159,9 +159,9 @@
 "aval' (V x) S = S x" |
 "aval' (Plus a1 a2) S = plus' (aval' a1 S) (aval' a2 S)"
 
-definition "step' = Step
-  (\<lambda>x e S. case S of None \<Rightarrow> None | Some S \<Rightarrow> Some(S(x := aval' e S)))
-  (\<lambda>b S. S)"
+definition "fa x e S = (case S of None \<Rightarrow> None | Some S \<Rightarrow> Some(S(x := aval' e S)))"
+
+definition "step' = Step fa (\<lambda>b S. S)"
 
 definition AI :: "com \<Rightarrow> 'av st option acom option" where
 "AI c = pfp (step' \<top>) (bot c)"
@@ -208,7 +208,8 @@
 
 lemma step_step': "step (\<gamma>\<^isub>o S) (\<gamma>\<^isub>c C) \<le> \<gamma>\<^isub>c (step' S C)"
 unfolding step_def step'_def
-by(rule gamma_Step_subcomm) (auto simp: aval'_sound in_gamma_update split: option.splits)
+by(rule gamma_Step_subcomm)
+  (auto simp: aval'_sound in_gamma_update fa_def split: option.splits)
 
 lemma AI_sound: "AI c = Some C \<Longrightarrow> CS c \<le> \<gamma>\<^isub>c C"
 proof(simp add: CS_def AI_def)
@@ -245,7 +246,8 @@
 
 lemma mono_step': "S1 \<le> S2 \<Longrightarrow> C1 \<le> C2 \<Longrightarrow> step' S1 C1 \<le> step' S2 C2"
 unfolding step'_def
-by(rule mono2_Step) (auto simp: mono_update mono_aval' split: option.split)
+by(rule mono2_Step)
+  (auto simp: mono_update mono_aval' fa_def split: option.split)
 
 end