1.1 --- a/src/HOL/IMP/Abs_Int1_const.thy	Tue Sep 18 03:24:51 2012 +0200
     1.2 +++ b/src/HOL/IMP/Abs_Int1_const.thy	Tue Sep 18 03:33:53 2012 +0200
     1.3 @@ -133,7 +133,7 @@
     1.4  
     1.5  interpretation Abs_Int_measure
     1.6  where \<gamma> = \<gamma>_const and num' = Const and plus' = plus_const
     1.7 -and m = m_const and h = "2"
     1.8 +and m = m_const and h = "1"
     1.9  proof
    1.10    case goal1 thus ?case by(auto simp: m_const_def split: const.splits)
    1.11  next

     2.1 --- a/src/HOL/IMP/Abs_Int1_parity.thy	Tue Sep 18 03:24:51 2012 +0200
     2.2 +++ b/src/HOL/IMP/Abs_Int1_parity.thy	Tue Sep 18 03:33:53 2012 +0200
     2.3 @@ -155,7 +155,7 @@
     2.4  
     2.5  interpretation Abs_Int_measure
     2.6  where \<gamma> = \<gamma>_parity and num' = num_parity and plus' = plus_parity
     2.7 -and m = m_parity and h = "2"
     2.8 +and m = m_parity and h = "1"
     2.9  proof
    2.10    case goal1 thus ?case by(auto simp add: m_parity_def le_parity_def)
    2.11  next