--- a/src/HOLCF/IOA/meta_theory/Traces.ML Tue Dec 23 11:56:09 1997 +0100
+++ b/src/HOLCF/IOA/meta_theory/Traces.ML Wed Dec 24 10:02:30 1997 +0100
@@ -179,7 +179,7 @@
by (asm_full_simp_tac (simpset() addsimps [executions_def]) 1);
by (pair_tac "x" 1);
by (rtac (execfrag_in_sig RS spec RS mp) 1);
-by (Auto_tac());
+by Auto_tac;
qed"exec_in_sig";
goalw thy [schedules_def,has_schedule_def]
@@ -213,7 +213,7 @@
by (strip_tac 1);
by (Seq_case_simp_tac "xa" 1);
by (pair_tac "a" 1);
-by (Auto_tac());
+by Auto_tac;
qed"execfrag_prefixclosed";
bind_thm ("exec_prefixclosed",conjI RS (execfrag_prefixclosed RS spec RS spec RS mp));
@@ -226,6 +226,6 @@
by (strip_tac 1);
by (Seq_case_simp_tac "s" 1);
by (pair_tac "a" 1);
-by (Auto_tac());
+by Auto_tac;
qed_spec_mp"exec_prefix2closed";