src/HOL/Integ/Bin.ML

 open Bin;
 
 (** extra rules for bin_succ, bin_pred, bin_add, bin_mult **)
 
 qed_goal "norm_Bcons_Plus_0" Bin.thy
-    "norm_Bcons Plus False = Plus"
+    "norm_Bcons PlusSign False = PlusSign"
  (fn _ => [(Simp_tac 1)]);
 
 qed_goal "norm_Bcons_Plus_1" Bin.thy
-    "norm_Bcons Plus True = Bcons Plus True"
+    "norm_Bcons PlusSign True = Bcons PlusSign True"
  (fn _ => [(Simp_tac 1)]);
 
 qed_goal "norm_Bcons_Minus_0" Bin.thy
-    "norm_Bcons Minus False = Bcons Minus False"
+    "norm_Bcons MinusSign False = Bcons MinusSign False"
  (fn _ => [(Simp_tac 1)]);
 
 qed_goal "norm_Bcons_Minus_1" Bin.thy
-    "norm_Bcons Minus True = Minus"
+    "norm_Bcons MinusSign True = MinusSign"
  (fn _ => [(Simp_tac 1)]);
 
 qed_goal "norm_Bcons_Bcons" Bin.thy
     "norm_Bcons (Bcons w x) b = Bcons (Bcons w x) b"
  (fn _ => [(Simp_tac 1)]);

 qed_goal "bin_add_Bcons_Bcons0" Bin.thy
     "bin_add (Bcons v False) (Bcons w y) = norm_Bcons (bin_add v w) y"
  (fn _ => [(simp_tac (!simpset addsimps [lemma]) 1)]);
 
 qed_goal "bin_add_Bcons_Plus" Bin.thy
-    "bin_add (Bcons v x) Plus = Bcons v x"
+    "bin_add (Bcons v x) PlusSign = Bcons v x"
  (fn _ => [(Simp_tac 1)]);
 
 qed_goal "bin_add_Bcons_Minus" Bin.thy
-    "bin_add (Bcons v x) Minus = bin_pred (Bcons v x)"
+    "bin_add (Bcons v x) MinusSign = bin_pred (Bcons v x)"
  (fn _ => [(Simp_tac 1)]);
 
 qed_goal "bin_add_Bcons_Bcons" Bin.thy
     "bin_add (Bcons v x) (Bcons w y) = \
 \    norm_Bcons(bin_add v (if x & y then (bin_succ w) else w)) (x~= y)"

   by (asm_full_simp_tac 
       (HOL_ss addsimps[zadd_assoc,zadd_0,zadd_0_right, 
                        zadd_zminus_inverse2]) 1); 
 val iob_eq_eq_diff_0 = result(); 
 
-goal Bin.thy "(integ_of_bin Plus = $# 0) = True"; 
+goal Bin.thy "(integ_of_bin PlusSign = $# 0) = True"; 
   by (stac iob_Plus 1); by (Simp_tac 1); 
 val iob_Plus_eq_0 = result(); 
 
-goal Bin.thy "(integ_of_bin Minus = $# 0) = False"; 
+goal Bin.thy "(integ_of_bin MinusSign = $# 0) = False"; 
   by (stac iob_Minus 1); 
   by (Simp_tac 1);
 val iob_Minus_not_eq_0 = result(); 
 
 goal Bin.thy 

     "integ_of_bin x < integ_of_bin y \
 \    = (integ_of_bin (bin_add x (bin_minus y)) < $# 0)";
   by (Simp_tac 1); 
 val iob_less_eq_diff_lt_0 = result(); 
 
-goal Bin.thy "(integ_of_bin Plus < $# 0) = False"; 
+goal Bin.thy "(integ_of_bin PlusSign < $# 0) = False"; 
   by (stac iob_Plus 1); by (Simp_tac 1); 
 val iob_Plus_not_lt_0 = result(); 
 
-goal Bin.thy "(integ_of_bin Minus < $# 0) = True"; 
+goal Bin.thy "(integ_of_bin MinusSign < $# 0) = True"; 
   by (stac iob_Minus 1); by (Simp_tac 1);
 val iob_Minus_lt_0 = result(); 
 
 goal Bin.thy 
     "(integ_of_bin (Bcons w x) < $# 0) = (integ_of_bin w < $# 0)";