changeset 58305 | 57752a91eec4 |
parent 57492 | 74bf65a1910a |
child 58316 | 18e6cb6a5297 |
--- a/src/HOL/IMP/Abs_Int_Den/Abs_Int_den1.thy Thu Sep 11 18:54:36 2014 +0200 +++ b/src/HOL/IMP/Abs_Int_Den/Abs_Int_den1.thy Thu Sep 11 18:54:36 2014 +0200 @@ -37,7 +37,7 @@ and filter_less': "filter_less' (n1<n2) a1 a2 = (a1',a2') \<Longrightarrow> n1 <: a1 \<Longrightarrow> n2 <: a2 \<Longrightarrow> n1 <: a1' \<and> n2 <: a2'" -datatype 'a up = bot | Up 'a +old_datatype 'a up = bot | Up 'a instantiation up :: (SL_top)SL_top begin