# HG changeset patch
# User blanchet
# Date 1367237223 -7200
# Node ID 6b82042690b5de671f851782519ed97fcd3599f0
# Parent  5f1dec4297dab649946f1dd213c9de2bd06b60a5# Parent  d694233adeaeb0c1bab29de8cbc0ca549d6e676c
merge

diff -r 5f1dec4297da -r 6b82042690b5 src/HOL/Cardinals/Cardinal_Arithmetic.thy
--- a/src/HOL/Cardinals/Cardinal_Arithmetic.thy	Mon Apr 29 14:06:37 2013 +0200
+++ b/src/HOL/Cardinals/Cardinal_Arithmetic.thy	Mon Apr 29 14:07:03 2013 +0200
@@ -366,10 +366,10 @@
 
 subsection {* Exponentiation *}
 
-definition cexp (infixr "^c" 80) where
+definition cexp (infixr "^c" 90) where
   "r1 ^c r2 \<equiv> |Func (Field r2) (Field r1)|"
 
-definition ccexp (infixr "^^c" 80) where
+definition ccexp (infixr "^^c" 90) where
   "r1 ^^c r2 \<equiv> |Pfunc (Field r2) (Field r1)|"
 
 lemma cexp_ordLeq_ccexp: "r1 ^c r2 \<le>o r1 ^^c r2"
diff -r 5f1dec4297da -r 6b82042690b5 src/HOL/IMP/Abs_Int0.thy
--- a/src/HOL/IMP/Abs_Int0.thy	Mon Apr 29 14:06:37 2013 +0200
+++ b/src/HOL/IMP/Abs_Int0.thy	Mon Apr 29 14:07:03 2013 +0200
@@ -167,9 +167,9 @@
 "aval' (V x) S = S x" |
 "aval' (Plus a1 a2) S = plus' (aval' a1 S) (aval' a2 S)"
 
-definition "fa x e S = (case S of None \<Rightarrow> None | Some S \<Rightarrow> Some(S(x := aval' e S)))"
+definition "asem 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 "step' = Step asem (\<lambda>b S. S)"
 
 lemma strip_step'[simp]: "strip(step' S C) = strip C"
 by(simp add: step'_def)
@@ -220,7 +220,7 @@
 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 fa_def split: option.splits)
+  (auto simp: aval'_sound in_gamma_update asem_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)
@@ -258,7 +258,7 @@
 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' fa_def split: option.split)
+  (auto simp: mono_update mono_aval' asem_def split: option.split)
 
 lemma mono_step'_top: "C \<le> C' \<Longrightarrow> step' \<top> C \<le> step' \<top> C'"
 by (metis mono_step' order_refl)
@@ -471,7 +471,7 @@
 lemma top_on_step': "top_on_acom C (-vars C) \<Longrightarrow> top_on_acom (step' \<top> C) (-vars C)"
 unfolding step'_def
 by(rule top_on_Step)
-  (auto simp add: top_option_def fa_def split: option.splits)
+  (auto simp add: top_option_def asem_def split: option.splits)
 
 lemma AI_Some_measure: "\<exists>C. AI c = Some C"
 unfolding AI_def