# HG changeset patch
# User paulson
# Date 914860004 -3600
# Node ID 1512f4b7d2e880e27c5d293d0d907e89d2d7821c
# Parent  c041fc54ab4c6e04add4d0c3821406c0318511fc
fixed comments

diff -r c041fc54ab4c -r 1512f4b7d2e8 src/HOL/Integ/Bin.ML
--- a/src/HOL/Integ/Bin.ML	Mon Dec 28 16:46:15 1998 +0100
+++ b/src/HOL/Integ/Bin.ML	Mon Dec 28 16:46:44 1998 +0100
@@ -80,7 +80,7 @@
  (fn _ => [(Simp_tac 1)]);
 
 
-(*** bin_add: binary multiplication ***)
+(*** bin_mult: binary multiplication ***)
 
 qed_goal "bin_mult_1" Bin.thy
     "bin_mult (v BIT True) w = bin_add (NCons (bin_mult v w) False) w"
@@ -124,9 +124,9 @@
 qed "integ_of_minus";
 
  
-val bin_add_simps = [bin_add_BIT_BIT,
-                     integ_of_succ, integ_of_pred];
+val bin_add_simps = [bin_add_BIT_BIT, integ_of_succ, integ_of_pred];
 
+(*This proof is complicated by the mutual recursion*)
 Goal "! w. integ_of(bin_add v w) = integ_of v + integ_of w";
 by (induct_tac "v" 1);
 by (simp_tac (simpset() addsimps bin_add_simps) 1);