src/HOL/Integ/Bin.ML

                      bin_add_Bcons_Minus,bin_add_Bcons_Bcons,
                      integ_of_bin_succ, integ_of_bin_pred,
                      integ_of_bin_norm_Bcons];
 val bin_simps = [iob_Plus,iob_Minus,iob_Bcons];
 
-goal Bin.thy
+Goal
     "! w. integ_of_bin(bin_add v w) = integ_of_bin v + integ_of_bin w";
 by (bin.induct_tac "v" 1);
 by (simp_tac (simpset() addsimps bin_add_simps) 1);
 by (simp_tac (simpset() addsimps bin_add_simps) 1);
 by (rtac allI 1);

 by (etac disjE 1);
 by (asm_simp_tac (simpset() addsimps (bin_add_simps @ zadd_ac)) 1);
 by (asm_simp_tac (simpset() addsimps (bin_add_simps @ zadd_ac)) 1);
 val integ_of_bin_add_lemma = result();
 
-goal Bin.thy "integ_of_bin(bin_add v w) = integ_of_bin v + integ_of_bin w";
+Goal "integ_of_bin(bin_add v w) = integ_of_bin v + integ_of_bin w";
 by (cut_facts_tac [integ_of_bin_add_lemma] 1);
 by (Fast_tac 1);
 qed "integ_of_bin_add";
 
 val bin_mult_simps = [integ_of_bin_minus, integ_of_bin_add,
                       integ_of_bin_norm_Bcons];
 
-goal Bin.thy "integ_of_bin(bin_mult v w) = integ_of_bin v * integ_of_bin w";
+Goal "integ_of_bin(bin_mult v w) = integ_of_bin v * integ_of_bin w";
 by (bin.induct_tac "v" 1);
 by (simp_tac (simpset() addsimps bin_mult_simps) 1);
 by (simp_tac (simpset() addsimps bin_mult_simps) 1);
 by (cut_inst_tac [("P","bool")] True_or_False 1);
 by (etac disjE 1);

 
 (** Simplification rules for comparison of binary numbers (Norbert Voelker) **) 
 
 Addsimps [zadd_assoc];
 
-goal Bin.thy  
+Goal  
     "(integ_of_bin x = integ_of_bin y) \ 
 \   = (integ_of_bin (bin_add x (bin_minus y)) = $# 0)"; 
   by (simp_tac (HOL_ss addsimps
                 [integ_of_bin_add, integ_of_bin_minus,zdiff_def]) 1); 
   by (rtac iffI 1); 

   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 PlusSign = $# 0) = True"; 
+Goal "(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 MinusSign = $# 0) = False"; 
+Goal "(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 
+Goal 
     "(integ_of_bin (Bcons w x) = $# 0) = (~x & integ_of_bin w = $# 0)"; 
   by (stac iob_Bcons 1);
   by (case_tac "x" 1); 
   by (ALLGOALS Asm_simp_tac); 
   by (ALLGOALS(asm_simp_tac (HOL_ss addsimps [integ_of_bin_add]))); 

   by (rtac notI 1); 
   by (dres_inst_tac [("f","(% z. z +  $# Suc (Suc (n + n)))")] arg_cong 1); 
   by (Asm_full_simp_tac 1); 
 val iob_Bcons_eq_0 = result(); 
 
-goalw Bin.thy [zless_def,zdiff_def] 
+Goalw [zless_def,zdiff_def] 
     "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 PlusSign < $# 0) = False"; 
+Goal "(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 MinusSign < $# 0) = True"; 
+Goal "(integ_of_bin MinusSign < $# 0) = True"; 
   by (stac iob_Minus 1); by (Simp_tac 1);
 val iob_Minus_lt_0 = result(); 
 
-goal Bin.thy 
+Goal 
     "(integ_of_bin (Bcons w x) < $# 0) = (integ_of_bin w < $# 0)"; 
   by (stac iob_Bcons 1);
   by (case_tac "x" 1); 
   by (ALLGOALS Asm_simp_tac); 
   by (ALLGOALS(asm_simp_tac (HOL_ss addsimps [integ_of_bin_add]))); 

   by (stac (zadd_zminus_inverse RS sym) 1); 
   by (rtac zadd_zless_mono1 1); 
   by (Simp_tac 1); 
 val iob_Bcons_lt_0 = result(); 
 
-goal Bin.thy
+Goal
   "integ_of_bin x <= integ_of_bin y \
 \  = ( integ_of_bin (bin_add x (bin_minus y)) < $# 0 \
 \    | integ_of_bin (bin_add x (bin_minus y)) = $# 0)";
 by (simp_tac (HOL_ss addsimps 
               [zle_eq_zless_or_eq,iob_less_eq_diff_lt_0,zdiff_def

           iob_Bcons_eq_0, iob_Plus_not_lt_0, iob_Minus_lt_0, iob_Bcons_lt_0];
 
 
 (*** Examples of performing binary arithmetic by simplification ***)
 
-goal Bin.thy "#13  +  #19 = #32";
-by (Simp_tac 1);
-result();
-
-goal Bin.thy "#1234  +  #5678 = #6912";
-by (Simp_tac 1);
-result();
-
-goal Bin.thy "#1359  +  #~2468 = #~1109";
-by (Simp_tac 1);
-result();
-
-goal Bin.thy "#93746 +  #~46375 = #47371";
-by (Simp_tac 1);
-result();
-
-goal Bin.thy "$~ #65745 = #~65745";
-by (Simp_tac 1);
-result();
-
-goal Bin.thy "$~ #~54321 = #54321";
-by (Simp_tac 1);
-result();
-
-goal Bin.thy "#13  *  #19 = #247";
-by (Simp_tac 1);
-result();
-
-goal Bin.thy "#~84  *  #51 = #~4284";
-by (Simp_tac 1);
-result();
-
-goal Bin.thy "#255  *  #255 = #65025";
-by (Simp_tac 1);
-result();
-
-goal Bin.thy "#1359  *  #~2468 = #~3354012";
-by (Simp_tac 1);
-result();
-
-goal Bin.thy "#89 * #10 ~= #889";  
-by (Simp_tac 1); 
-result();
-
-goal Bin.thy "#13 < #18 - #4";  
-by (Simp_tac 1); 
-result();
-
-goal Bin.thy "#~345 < #~242 + #~100";  
-by (Simp_tac 1); 
-result();
-
-goal Bin.thy "#13557456 < #18678654";  
-by (Simp_tac 1); 
-result();
-
-goal Bin.thy "#999999 <= (#1000001 + #1)-#2";  
-by (Simp_tac 1); 
-result();
-
-goal Bin.thy "#1234567 <= #1234567";  
-by (Simp_tac 1); 
-result();
+Goal "#13  +  #19 = #32";
+by (Simp_tac 1);
+result();
+
+Goal "#1234  +  #5678 = #6912";
+by (Simp_tac 1);
+result();
+
+Goal "#1359  +  #~2468 = #~1109";
+by (Simp_tac 1);
+result();
+
+Goal "#93746 +  #~46375 = #47371";
+by (Simp_tac 1);
+result();
+
+Goal "$~ #65745 = #~65745";
+by (Simp_tac 1);
+result();
+
+Goal "$~ #~54321 = #54321";
+by (Simp_tac 1);
+result();
+
+Goal "#13  *  #19 = #247";
+by (Simp_tac 1);
+result();
+
+Goal "#~84  *  #51 = #~4284";
+by (Simp_tac 1);
+result();
+
+Goal "#255  *  #255 = #65025";
+by (Simp_tac 1);
+result();
+
+Goal "#1359  *  #~2468 = #~3354012";
+by (Simp_tac 1);
+result();
+
+Goal "#89 * #10 ~= #889";  
+by (Simp_tac 1); 
+result();
+
+Goal "#13 < #18 - #4";  
+by (Simp_tac 1); 
+result();
+
+Goal "#~345 < #~242 + #~100";  
+by (Simp_tac 1); 
+result();
+
+Goal "#13557456 < #18678654";  
+by (Simp_tac 1); 
+result();
+
+Goal "#999999 <= (#1000001 + #1)-#2";  
+by (Simp_tac 1); 
+result();
+
+Goal "#1234567 <= #1234567";  
+by (Simp_tac 1); 
+result();