equal
deleted
inserted
replaced
119 apply (clarsimp simp add: nth_sshiftr1 word_size) |
119 apply (clarsimp simp add: nth_sshiftr1 word_size) |
120 apply safe |
120 apply safe |
121 apply arith |
121 apply arith |
122 apply arith |
122 apply arith |
123 apply (erule thin_rl) |
123 apply (erule thin_rl) |
124 apply (case_tac nat) |
124 apply (case_tac n) |
125 apply safe |
125 apply safe |
126 apply simp |
126 apply simp |
127 apply simp |
127 apply simp |
128 apply (erule thin_rl) |
128 apply (erule thin_rl) |
129 apply (case_tac nat) |
129 apply (case_tac n) |
130 apply safe |
130 apply safe |
131 apply simp |
131 apply simp |
132 apply simp |
132 apply simp |
133 apply arith+ |
133 apply arith+ |
134 done |
134 done |