src/HOL/List.ML
changeset 11265 4f2e6c87a57f
parent 10832 e33b47e4246d
child 11289 65782388cf40
     1.1 --- a/src/HOL/List.ML	Tue Apr 24 12:19:01 2001 +0200
     1.2 +++ b/src/HOL/List.ML	Tue Apr 24 12:19:58 2001 +0200
     1.3 @@ -1374,6 +1374,7 @@
     1.4  qed "wf_lex";
     1.5  AddSIs [wf_lex];
     1.6  
     1.7 +
     1.8  Goal
     1.9   "lexn r n = \
    1.10  \ {(xs,ys). length xs = n & length ys = n & \
    1.11 @@ -1381,15 +1382,14 @@
    1.12  by (induct_tac "n" 1);
    1.13   by (Simp_tac 1);
    1.14   by (Blast_tac 1);
    1.15 -by (asm_full_simp_tac (simpset() 
    1.16 -				addsimps [lex_prod_def]) 1);
    1.17 -by (auto_tac (claset(), simpset()));
    1.18 +by (asm_full_simp_tac (simpset() addsimps [image_Collect, lex_prod_def]) 1);
    1.19 +by Auto_tac;
    1.20    by (Blast_tac 1);
    1.21   by (rename_tac "a xys x xs' y ys'" 1);
    1.22   by (res_inst_tac [("x","a#xys")] exI 1);
    1.23   by (Simp_tac 1);
    1.24  by (case_tac "xys" 1);
    1.25 - by (ALLGOALS (asm_full_simp_tac (simpset())));
    1.26 + by (ALLGOALS Asm_full_simp_tac);
    1.27  by (Blast_tac 1);
    1.28  qed "lexn_conv";
    1.29