src/HOL/IMP/Abs_Int_ITP/Abs_Int3_ITP.thy

--- a/src/HOL/IMP/Abs_Int_ITP/Abs_Int3_ITP.thy	Wed Feb 19 22:05:05 2014 +0100
+++ b/src/HOL/IMP/Abs_Int_ITP/Abs_Int3_ITP.thy	Wed Feb 19 22:05:15 2014 +0100
@@ -229,7 +229,7 @@
 where \<gamma> = \<gamma>_ivl and num' = num_ivl and plus' = plus_ivl
 and test_num' = in_ivl
 and filter_plus' = filter_plus_ivl and filter_less' = filter_less_ivl
-defines AI_ivl' is AI_wn
+defining AI_ivl' = AI_wn
 ..