| changeset 55600 | 3c7610b8dcfc |
| parent 55599 | 6535c537b243 |
| child 61179 | 16775cad1a5c |
--- a/src/HOL/IMP/Abs_Int3.thy Wed Feb 19 22:05:05 2014 +0100 +++ b/src/HOL/IMP/Abs_Int3.thy Wed Feb 19 22:05:15 2014 +0100 @@ -264,7 +264,7 @@ where \<gamma> = \<gamma>_ivl and num' = num_ivl and plus' = "op +" and test_num' = in_ivl and inv_plus' = inv_plus_ivl and inv_less' = inv_less_ivl -defines AI_wn_ivl is AI_wn +defining AI_wn_ivl = AI_wn ..