--- a/src/HOLCF/IOA/meta_theory/Traces.ML Mon Jun 23 10:35:49 1997 +0200
+++ b/src/HOLCF/IOA/meta_theory/Traces.ML Mon Jun 23 10:42:03 1997 +0200
@@ -71,9 +71,9 @@
\ `x) \
\ ))";
by (rtac trans 1);
-br fix_eq2 1;
-br is_exec_fragC_def 1;
-br beta_cfun 1;
+by (rtac fix_eq2 1);
+by (rtac is_exec_fragC_def 1);
+by (rtac beta_cfun 1);
by (simp_tac (!simpset addsimps [flift1_def]) 1);
qed"is_exec_fragC_unfold";
@@ -90,7 +90,7 @@
goal thy "(is_exec_fragC A`(pr>>xs)) s = \
\ (Def ((s,pr):trans_of A) \
\ andalso (is_exec_fragC A`xs)(snd pr))";
-br trans 1;
+by (rtac trans 1);
by (stac is_exec_fragC_unfold 1);
by (asm_full_simp_tac (!simpset addsimps [Cons_def,flift1_def]) 1);
by (Simp_tac 1);
@@ -178,8 +178,8 @@
by (asm_full_simp_tac (!simpset addsimps [executions_def]) 1);
by (pair_tac "x" 1);
-br (execfrag_in_sig RS spec RS mp) 1;
-auto();
+by (rtac (execfrag_in_sig RS spec RS mp) 1);
+by (Auto_tac());
qed"exec_in_sig";
goalw thy [schedules_def,has_schedule_def]
@@ -200,7 +200,7 @@
by (strip_tac 1);
by (Seq_case_simp_tac "xa" 1);
by (pair_tac "a" 1);
-auto();
+by (Auto_tac());
qed"execfrag_prefixclosed";
bind_thm ("exec_prefixclosed",conjI RS (execfrag_prefixclosed RS spec RS spec RS mp));
@@ -213,6 +213,6 @@
by (strip_tac 1);
by (Seq_case_simp_tac "s" 1);
by (pair_tac "a" 1);
-auto();
+by (Auto_tac());
qed_spec_mp"exec_prefix2closed";