src/HOLCF/IOA/meta_theory/Traces.ML
changeset 4477 b3e5857d8d99
parent 4423 a129b817b58a
child 4536 74f7c556fd90
--- 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";