src/HOL/Lex/RegSet_of_nat_DA.ML

 
 goal Nat.thy "!!n. [| n < Suc k; n ~= k |] ==> n < k";
 by (etac nat_neqE 1);
 by (ALLGOALS trans_tac);
 val lemma = result();
-
 
 Goal
  "!i j xs. xs : regset d i j k = \
 \          ((!n:set(butlast(trace d i xs)). n < k) & deltas d xs i = j)";
 by (induct_tac "k" 1);

   by (Asm_simp_tac 2);
  by (EVERY[dtac bspec 1, atac 2]);
  by (asm_simp_tac (simpset() addsimps [image_eqI,in_set_butlast_concatI]) 1);
 by (rtac ballI 1);
 by (rtac lemma 1);
- by (Asm_simp_tac 2);
-by (EVERY[dtac bspec 1, atac 2]);
-by (Asm_simp_tac 1);
+ by (Auto_tac);
 qed_spec_mp "regset_spec";
 
 Goalw [bounded_def]
  "bounded d k ==> !i. i < k --> (!n:set(trace d i xs). n < k)";
 by (induct_tac "xs" 1);