# HG changeset patch
# User nipkow
# Date 1347931491 -7200
# Node ID 3f4104ccca776f9070aeea0acec1aa82ccfe9356
# Parent  bf491a1c15c2dc559e6dfaad9bd58217b8535ab8
beautified names

diff -r bf491a1c15c2 -r 3f4104ccca77 src/HOL/IMP/Abs_Int1.thy
--- a/src/HOL/IMP/Abs_Int1.thy	Tue Sep 18 01:55:13 2012 +0200
+++ b/src/HOL/IMP/Abs_Int1.thy	Tue Sep 18 03:24:51 2012 +0200
@@ -233,7 +233,8 @@
 assumes h: "m x \<le> h"
 begin
 
-definition "m_st S = (\<Sum> x \<in> dom S. m(fun S x))"
+definition m_st :: "'av st \<Rightarrow> nat" ("m\<^isub>s\<^isub>t") where
+"m_st S = (\<Sum> x \<in> dom S. m(fun S x))"
 
 lemma m_st_h: "x \<in> L X \<Longrightarrow> finite X \<Longrightarrow> m_st x \<le> h * card X"
 by(simp add: L_st_def m_st_def)
@@ -258,7 +259,7 @@
 qed
 
 
-definition m_o :: "nat \<Rightarrow> 'av st option \<Rightarrow> nat" where
+definition m_o :: "nat \<Rightarrow> 'av st option \<Rightarrow> nat" ("m\<^isub>o") where
 "m_o d opt = (case opt of None \<Rightarrow> h*d+1 | Some S \<Rightarrow> m_st S)"
 
 lemma m_o_h: "ost \<in> L X \<Longrightarrow> finite X \<Longrightarrow> m_o (card X) ost \<le> (h*card X + 1)"
@@ -287,7 +288,7 @@
 qed
 
 
-definition m_c :: "'av st option acom \<Rightarrow> nat" where
+definition m_c :: "'av st option acom \<Rightarrow> nat" ("m\<^isub>c") where
 "m_c C = (\<Sum>i<size(annos C). m_o (card(vars(strip C))) (annos C ! i))"
 
 lemma m_c_h: assumes "C \<in> L(vars(strip C))"