src/HOL/List.ML
changeset 6162 484adda70b65
parent 6141 a6922171b396
child 6306 81e7fbf61db2
     1.1 --- a/src/HOL/List.ML	Fri Jan 29 16:23:56 1999 +0100
     1.2 +++ b/src/HOL/List.ML	Fri Jan 29 16:26:12 1999 +0100
     1.3 @@ -384,7 +384,7 @@
     1.4  
     1.5  val prems = Goal "[| P []; !!x xs. P xs ==> P(xs@[x]) |] ==> P xs";
     1.6  by (stac (rev_rev_ident RS sym) 1);
     1.7 -br(read_instantiate [("P","%xs. ?P(rev xs)")]list.induct)1;
     1.8 +by (res_inst_tac [("list", "rev xs")] list.induct 1);
     1.9  by (ALLGOALS Simp_tac);
    1.10  by (resolve_tac prems 1);
    1.11  by (eresolve_tac prems 1);
    1.12 @@ -571,7 +571,7 @@
    1.13  section "nth";
    1.14  
    1.15  Goal "(x#xs)!n = (case n of 0 => x | Suc m => xs!m)";
    1.16 -by(simp_tac (simpset() addsplits [nat.split]) 1);
    1.17 +by (simp_tac (simpset() addsplits [nat.split]) 1);
    1.18  qed "nth_Cons";
    1.19  
    1.20  Goal "!xs. (xs@ys)!n = (if n < length xs then xs!n else ys!(n - length xs))";
    1.21 @@ -630,9 +630,9 @@
    1.22  Addsimps [length_list_update];
    1.23  
    1.24  Goal "!i j. i < length xs  --> (xs[i:=x])!j = (if i=j then x else xs!j)";
    1.25 -by(induct_tac "xs" 1);
    1.26 - by(Simp_tac 1);
    1.27 -by(auto_tac (claset(), simpset() addsimps [nth_Cons] addsplits [nat.split]));
    1.28 +by (induct_tac "xs" 1);
    1.29 + by (Simp_tac 1);
    1.30 +by (auto_tac (claset(), simpset() addsimps [nth_Cons] addsplits [nat.split]));
    1.31  qed_spec_mp "nth_list_update";
    1.32  
    1.33  
    1.34 @@ -874,13 +874,13 @@
    1.35  
    1.36  (* Does not terminate! *)
    1.37  Goal "[i..j(] = (if i<j then i#[Suc i..j(] else [])";
    1.38 -by(induct_tac "j" 1);
    1.39 +by (induct_tac "j" 1);
    1.40  by Auto_tac;
    1.41  qed "upt_rec";
    1.42  
    1.43  Goal "j<=i ==> [i..j(] = []";
    1.44 -by(stac upt_rec 1);
    1.45 -by(Asm_simp_tac 1);
    1.46 +by (stac upt_rec 1);
    1.47 +by (Asm_simp_tac 1);
    1.48  qed "upt_conv_Nil";
    1.49  Addsimps [upt_conv_Nil];
    1.50  
    1.51 @@ -889,27 +889,27 @@
    1.52  qed "upt_Suc";
    1.53  
    1.54  Goal "i<j ==> [i..j(] = i#[Suc i..j(]";
    1.55 -br trans 1;
    1.56 -by(stac upt_rec 1);
    1.57 -br refl 2;
    1.58 +by (rtac trans 1);
    1.59 +by (stac upt_rec 1);
    1.60 +by (rtac refl 2);
    1.61  by (Asm_simp_tac 1);
    1.62  qed "upt_conv_Cons";
    1.63  
    1.64  Goal "length [i..j(] = j-i";
    1.65 -by(induct_tac "j" 1);
    1.66 +by (induct_tac "j" 1);
    1.67   by (Simp_tac 1);
    1.68 -by(asm_simp_tac (simpset() addsimps [Suc_diff_le]) 1);
    1.69 +by (asm_simp_tac (simpset() addsimps [Suc_diff_le]) 1);
    1.70  qed "length_upt";
    1.71  Addsimps [length_upt];
    1.72  
    1.73  Goal "i+k < j --> [i..j(] ! k = i+k";
    1.74 -by(induct_tac "j" 1);
    1.75 - by(Simp_tac 1);
    1.76 -by(asm_simp_tac (simpset() addsimps [nth_append,less_diff_conv]@add_ac) 1);
    1.77 -by(Clarify_tac 1);
    1.78 -by(subgoal_tac "n=i+k" 1);
    1.79 - by(Asm_simp_tac 2);
    1.80 -by(Asm_simp_tac 1);
    1.81 +by (induct_tac "j" 1);
    1.82 + by (Simp_tac 1);
    1.83 +by (asm_simp_tac (simpset() addsimps [nth_append,less_diff_conv]@add_ac) 1);
    1.84 +by (Clarify_tac 1);
    1.85 +by (subgoal_tac "n=i+k" 1);
    1.86 + by (Asm_simp_tac 2);
    1.87 +by (Asm_simp_tac 1);
    1.88  qed_spec_mp "nth_upt";
    1.89  Addsimps [nth_upt];
    1.90