| changeset 52504 | 52cd8bebc3b6 |
| parent 51826 | 054a40461449 |
| child 55599 | 6535c537b243 |
--- a/src/HOL/IMP/Abs_Int1_const.thy Tue Jul 02 20:47:32 2013 +0200 +++ b/src/HOL/IMP/Abs_Int1_const.thy Wed Jul 03 16:07:00 2013 +0200 @@ -53,7 +53,7 @@ end -interpretation Val_abs +interpretation Val_semilattice where \<gamma> = \<gamma>_const and num' = Const and plus' = plus_const proof case goal1 thus ?case