src/HOL/Word/BinOperations.thy
changeset 25112 98824cc791c0
parent 24465 70f0214b3ecc
child 25762 c03e9d04b3e4
     1.1 --- a/src/HOL/Word/BinOperations.thy	Sat Oct 20 12:09:30 2007 +0200
     1.2 +++ b/src/HOL/Word/BinOperations.thy	Sat Oct 20 12:09:33 2007 +0200
     1.3 @@ -353,7 +353,6 @@
     1.4    "!!w m. m ~= n ==> 
     1.5      bin_sc m c (bin_sc n b w) = bin_sc n b (bin_sc m c w)"
     1.6    apply (induct n)
     1.7 -   apply safe
     1.8     apply (case_tac [!] m)
     1.9       apply auto
    1.10    done