1.1 --- a/src/HOL/IMP/Abs_Int1.thy	Tue Sep 18 01:55:13 2012 +0200
     1.2 +++ b/src/HOL/IMP/Abs_Int1.thy	Tue Sep 18 03:24:51 2012 +0200
     1.3 @@ -233,7 +233,8 @@
     1.4  assumes h: "m x \<le> h"
     1.5  begin
     1.6  
     1.7 -definition "m_st S = (\<Sum> x \<in> dom S. m(fun S x))"
     1.8 +definition m_st :: "'av st \<Rightarrow> nat" ("m\<^isub>s\<^isub>t") where
     1.9 +"m_st S = (\<Sum> x \<in> dom S. m(fun S x))"
    1.10  
    1.11  lemma m_st_h: "x \<in> L X \<Longrightarrow> finite X \<Longrightarrow> m_st x \<le> h * card X"
    1.12  by(simp add: L_st_def m_st_def)
    1.13 @@ -258,7 +259,7 @@
    1.14  qed
    1.15  
    1.16  
    1.17 -definition m_o :: "nat \<Rightarrow> 'av st option \<Rightarrow> nat" where
    1.18 +definition m_o :: "nat \<Rightarrow> 'av st option \<Rightarrow> nat" ("m\<^isub>o") where
    1.19  "m_o d opt = (case opt of None \<Rightarrow> h*d+1 | Some S \<Rightarrow> m_st S)"
    1.20  
    1.21  lemma m_o_h: "ost \<in> L X \<Longrightarrow> finite X \<Longrightarrow> m_o (card X) ost \<le> (h*card X + 1)"
    1.22 @@ -287,7 +288,7 @@
    1.23  qed
    1.24  
    1.25  
    1.26 -definition m_c :: "'av st option acom \<Rightarrow> nat" where
    1.27 +definition m_c :: "'av st option acom \<Rightarrow> nat" ("m\<^isub>c") where
    1.28  "m_c C = (\<Sum>i<size(annos C). m_o (card(vars(strip C))) (annos C ! i))"
    1.29  
    1.30  lemma m_c_h: assumes "C \<in> L(vars(strip C))"