bind_thms;
authorwenzelm
Wed Sep 01 21:25:55 1999 +0200 (1999-09-01)
changeset 742880838c2af97b
parent 7427 e5a5d59dd513
child 7429 8f284fbb8728
bind_thms;
src/HOL/Arith.ML
src/HOL/Integ/IntDef.ML
src/HOL/Real/RealDef.ML
     1.1 --- a/src/HOL/Arith.ML	Wed Sep 01 21:25:17 1999 +0200
     1.2 +++ b/src/HOL/Arith.ML	Wed Sep 01 21:25:55 1999 +0200
     1.3 @@ -74,7 +74,7 @@
     1.4  qed "add_left_commute";
     1.5  
     1.6  (*Addition is an AC-operator*)
     1.7 -val add_ac = [add_assoc, add_commute, add_left_commute];
     1.8 +bind_thms ("add_ac", [add_assoc, add_commute, add_left_commute]);
     1.9  
    1.10  Goal "(k + m = k + n) = (m=(n::nat))";
    1.11  by (induct_tac "k" 1);
    1.12 @@ -329,7 +329,7 @@
    1.13  by (rtac (mult_commute RS arg_cong) 1);
    1.14  qed "mult_left_commute";
    1.15  
    1.16 -val mult_ac = [mult_assoc,mult_commute,mult_left_commute];
    1.17 +bind_thms ("mult_ac", [mult_assoc,mult_commute,mult_left_commute]);
    1.18  
    1.19  Goal "(m*n = 0) = (m=0 | n=0)";
    1.20  by (induct_tac "m" 1);
    1.21 @@ -1006,7 +1006,8 @@
    1.22  
    1.23  (* proof method setup *)
    1.24  
    1.25 -val arith_method = Method.METHOD (fn facts => FIRSTGOAL (Method.same_tac facts THEN' arith_tac));
    1.26 +val arith_method =
    1.27 +  Method.METHOD (fn facts => FIRSTGOAL (Method.insert_tac facts THEN' arith_tac));
    1.28  
    1.29  val arith_setup =
    1.30   [Method.add_methods
     2.1 --- a/src/HOL/Integ/IntDef.ML	Wed Sep 01 21:25:17 1999 +0200
     2.2 +++ b/src/HOL/Integ/IntDef.ML	Wed Sep 01 21:25:55 1999 +0200
     2.3 @@ -188,7 +188,7 @@
     2.4  qed "zadd_left_commute";
     2.5  
     2.6  (*Integer addition is an AC operator*)
     2.7 -val zadd_ac = [zadd_assoc,zadd_commute,zadd_left_commute];
     2.8 +bind_thms ("zadd_ac", [zadd_assoc,zadd_commute,zadd_left_commute]);
     2.9  
    2.10  Goalw [int_def] "(int m) + (int n) = int (m + n)";
    2.11  by (simp_tac (simpset() addsimps [zadd]) 1);
    2.12 @@ -325,7 +325,7 @@
    2.13  qed "zmult_left_commute";
    2.14  
    2.15  (*Integer multiplication is an AC operator*)
    2.16 -val zmult_ac = [zmult_assoc, zmult_commute, zmult_left_commute];
    2.17 +bind_thms ("zmult_ac", [zmult_assoc, zmult_commute, zmult_left_commute]);
    2.18  
    2.19  Goal "((z1::int) + z2) * w = (z1 * w) + (z2 * w)";
    2.20  by (res_inst_tac [("z","z1")] eq_Abs_Integ 1);
     3.1 --- a/src/HOL/Real/RealDef.ML	Wed Sep 01 21:25:17 1999 +0200
     3.2 +++ b/src/HOL/Real/RealDef.ML	Wed Sep 01 21:25:55 1999 +0200
     3.3 @@ -194,7 +194,7 @@
     3.4  qed "real_add_left_commute";
     3.5  
     3.6  (* real addition is an AC operator *)
     3.7 -val real_add_ac = [real_add_assoc,real_add_commute,real_add_left_commute];
     3.8 +bind_thms ("real_add_ac", [real_add_assoc,real_add_commute,real_add_left_commute]);
     3.9  
    3.10  Goalw [real_of_preal_def,real_zero_def] "0r + z = z";
    3.11  by (res_inst_tac [("z","z")] eq_Abs_real 1);
    3.12 @@ -361,7 +361,7 @@
    3.13             rtac (real_mult_commute RS arg_cong) 1]);
    3.14  
    3.15  (* real multiplication is an AC operator *)
    3.16 -val real_mult_ac = [real_mult_assoc, real_mult_commute, real_mult_left_commute];
    3.17 +bind_thms ("real_mult_ac", [real_mult_assoc, real_mult_commute, real_mult_left_commute]);
    3.18  
    3.19  Goalw [real_one_def,pnat_one_def] "1r * z = z";
    3.20  by (res_inst_tac [("z","z")] eq_Abs_real 1);
    3.21 @@ -880,7 +880,7 @@
    3.22  by (assume_tac 1);
    3.23  qed "real_leD";
    3.24  
    3.25 -val real_leE = make_elim real_leD;
    3.26 +bind_thm ("real_leE", make_elim real_leD);
    3.27  
    3.28  Goal "(~(w < z)) = (z <= (w::real))";
    3.29  by (blast_tac (claset() addSIs [real_leI,real_leD]) 1);