| changeset 14264 | 3d0c6238162a |
| parent 13491 | ddf6ae639f21 |
| child 14266 | 08b34c902618 |
--- a/src/HOL/Integ/Bin.ML Thu Nov 20 10:41:39 2003 +0100 +++ b/src/HOL/Integ/Bin.ML Thu Nov 20 10:42:00 2003 +0100 @@ -254,6 +254,8 @@ by (Simp_tac 1); qed "nonzero_number_of_Min"; +fun int_case_tac x = res_inst_tac [("z",x)] int_cases; + Goalw [iszero_def] "iszero (number_of (w BIT x)) = (~x & iszero (number_of w::int))"; by (int_case_tac "number_of w" 1);