--- a/src/HOLCF/IOA/meta_theory/TLS.ML Thu Jan 28 18:28:06 1999 +0100
+++ b/src/HOLCF/IOA/meta_theory/TLS.ML Fri Jan 29 16:23:56 1999 +0100
@@ -86,21 +86,21 @@
after the translation via ex2seq !! *)
Goalw [Init_def,Next_def,temp_sat_def,satisfies_def,IMPLIES_def,AND_def]
- "!! A. [| ! s a t. (P s) & s-a--A-> t --> (Q t) |]\
+ "[| ! s a t. (P s) & s-a--A-> t --> (Q t) |]\
\ ==> ex |== (Init (%(s,a,t). P s) .& Init (%(s,a,t). s -a--A-> t) \
\ .--> (Next (Init (%(s,a,t).Q s))))";
by (clarify_tac set_cs 1);
by (asm_full_simp_tac (simpset() setloop split_tac [expand_if]) 1);
(* TL = UU *)
-br conjI 1;
+by (rtac conjI 1);
by (pair_tac "ex" 1);
by (Seq_case_simp_tac "y" 1);
by (pair_tac "a" 1);
by (Seq_case_simp_tac "s" 1);
by (pair_tac "a" 1);
(* TL = nil *)
-br conjI 1;
+by (rtac conjI 1);
by (pair_tac "ex" 1);
by (Seq_case_simp_tac "y" 1);
by (asm_full_simp_tac (simpset() addsimps [unlift_def])1);