diff -r 7b5efef2ca74 -r 6b995dad8a9d src/HOL/Lex/RegSet_of_nat_DA.ML
--- a/src/HOL/Lex/RegSet_of_nat_DA.ML	Fri Jul 03 10:36:47 1998 +0200
+++ b/src/HOL/Lex/RegSet_of_nat_DA.ML	Fri Jul 03 10:37:04 1998 +0200
@@ -187,29 +187,29 @@
 qed_spec_mp "regset_spec";
 
 Goalw [bounded_def]
- "!!d. bounded d k ==> !i. i < k --> (!n:set(trace d i xs). n < k)";
+ "bounded d k ==> !i. i < k --> (!n:set(trace d i xs). n < k)";
 by (induct_tac "xs" 1);
  by (ALLGOALS Simp_tac);
 by (Blast_tac 1);
 qed_spec_mp "trace_below";
 
-Goal "!!d. [| bounded d k; i < k; j < k |] ==> \
-\         regset d i j k = {xs. deltas d xs i = j}";
+Goal "[| bounded d k; i < k; j < k |] ==> \
+\     regset d i j k = {xs. deltas d xs i = j}";
 by (rtac set_ext 1);
 by (simp_tac (simpset() addsimps [regset_spec]) 1);
 by (blast_tac (claset() addDs [trace_below,in_set_butlastD]) 1);
 qed "regset_below";
 
 Goalw [bounded_def]
- "!!d. bounded d k ==> !i. i < k --> deltas d w i < k";
+ "bounded d k ==> !i. i < k --> deltas d w i < k";
 by (induct_tac "w" 1);
  by (ALLGOALS Simp_tac);
 by (Blast_tac 1);
 qed_spec_mp "deltas_below";
 
 Goalw [regset_of_DA_def]
- "!!d. [| bounded (next A) k; start A < k; j < k |] ==> \
-\      w : regset_of_DA A k = accepts A w";
+ "[| bounded (next A) k; start A < k; j < k |] ==> \
+\ w : regset_of_DA A k = accepts A w";
 by(asm_simp_tac (simpset() addcongs [conj_cong] addsimps
  [regset_below,deltas_below,accepts_def,delta_def]) 1);
 qed "regset_DA_equiv";