changeset 49433 | 1095f240146a |
parent 49399 | a9d9f3483b71 |
child 50995 | 3371f5ee4ace |
--- a/src/HOL/IMP/Abs_Int1_const.thy Tue Sep 18 03:24:51 2012 +0200 +++ b/src/HOL/IMP/Abs_Int1_const.thy Tue Sep 18 03:33:53 2012 +0200 @@ -133,7 +133,7 @@ interpretation Abs_Int_measure where \<gamma> = \<gamma>_const and num' = Const and plus' = plus_const -and m = m_const and h = "2" +and m = m_const and h = "1" proof case goal1 thus ?case by(auto simp: m_const_def split: const.splits) next