--- a/src/HOL/Word/BinGeneral.thy Tue Aug 21 16:52:47 2007 +0200
+++ b/src/HOL/Word/BinGeneral.thy Tue Aug 21 17:20:41 2007 +0200
@@ -29,13 +29,9 @@
termination
apply (relation "measure (nat o abs o fst)")
apply simp
- apply (simp add: Pls_def brlem)
- apply (clarsimp simp: bin_rl_char pred_def)
- apply (frule thin_rl [THEN refl [THEN bin_abs_lem [rule_format]]])
- apply (unfold Pls_def Min_def number_of_eq)
- prefer 2
- apply (erule asm_rl)
- apply auto
+ apply (case_tac bin rule: bin_exhaust)
+ apply (frule bin_abs_lem)
+ apply simp
done
constdefs