# HG changeset patch # User nipkow # Date 1360668164 -3600 # Node ID 0a6d84c41dbf7272be76f88ba6df1fd6b4888573 # Parent e7b54119c436cb3aa07e0976fa20dc87031e7a74 tuned identifier diff -r e7b54119c436 -r 0a6d84c41dbf src/HOL/IMP/Abs_Int2.thy --- a/src/HOL/IMP/Abs_Int2.thy Tue Feb 12 11:54:29 2013 +0100 +++ b/src/HOL/IMP/Abs_Int2.thy Tue Feb 12 12:22:44 2013 +0100 @@ -105,8 +105,8 @@ (if res then bfilter b1 True (bfilter b2 True S) else bfilter b1 False S \ bfilter b2 False S)" | "bfilter (Less e1 e2) res S = - (let (res1,res2) = filter_less' res (aval'' e1 S) (aval'' e2 S) - in afilter e1 res1 (afilter e2 res2 S))" + (let (a1,a2) = filter_less' res (aval'' e1 S) (aval'' e2 S) + in afilter e1 a1 (afilter e2 a2 S))" lemma afilter_in_L: "S \ L X \ vars e \ X \ afilter e a S \ L X" by(induction e arbitrary: a S)