--- a/src/HOL/IMP/Abs_State.thy Fri Sep 21 13:39:30 2012 +0200
+++ b/src/HOL/IMP/Abs_State.thy Fri Sep 21 13:56:57 2012 +0200
@@ -184,16 +184,16 @@
locale Gamma = Val_abs where \<gamma>=\<gamma> for \<gamma> :: "'av::semilattice \<Rightarrow> val set"
begin
-abbreviation \<gamma>\<^isub>f :: "'av st \<Rightarrow> state set"
-where "\<gamma>\<^isub>f == \<gamma>_st \<gamma>"
+abbreviation \<gamma>\<^isub>s :: "'av st \<Rightarrow> state set"
+where "\<gamma>\<^isub>s == \<gamma>_st \<gamma>"
abbreviation \<gamma>\<^isub>o :: "'av st option \<Rightarrow> state set"
-where "\<gamma>\<^isub>o == \<gamma>_option \<gamma>\<^isub>f"
+where "\<gamma>\<^isub>o == \<gamma>_option \<gamma>\<^isub>s"
abbreviation \<gamma>\<^isub>c :: "'av st option acom \<Rightarrow> state set acom"
where "\<gamma>\<^isub>c == map_acom \<gamma>\<^isub>o"
-lemma gamma_f_Top[simp]: "\<gamma>\<^isub>f (top c) = UNIV"
+lemma gamma_s_Top[simp]: "\<gamma>\<^isub>s (top c) = UNIV"
by(auto simp: top_st_def \<gamma>_st_def)
lemma gamma_o_Top[simp]: "\<gamma>\<^isub>o (top c) = UNIV"
@@ -201,13 +201,13 @@
(* FIXME (maybe also le \<rightarrow> sqle?) *)
-lemma mono_gamma_f: "f \<sqsubseteq> g \<Longrightarrow> \<gamma>\<^isub>f f \<subseteq> \<gamma>\<^isub>f g"
+lemma mono_gamma_s: "f \<sqsubseteq> g \<Longrightarrow> \<gamma>\<^isub>s f \<subseteq> \<gamma>\<^isub>s g"
apply(simp add:\<gamma>_st_def subset_iff le_st_def split: if_splits)
by (metis mono_gamma subsetD)
lemma mono_gamma_o:
"S1 \<sqsubseteq> S2 \<Longrightarrow> \<gamma>\<^isub>o S1 \<subseteq> \<gamma>\<^isub>o S2"
-by(induction S1 S2 rule: le_option.induct)(simp_all add: mono_gamma_f)
+by(induction S1 S2 rule: le_option.induct)(simp_all add: mono_gamma_s)
lemma mono_gamma_c: "C1 \<sqsubseteq> C2 \<Longrightarrow> \<gamma>\<^isub>c C1 \<le> \<gamma>\<^isub>c C2"
by (induction C1 C2 rule: le_acom.induct) (simp_all add:mono_gamma_o)