src/HOLCF/IOA/meta_theory/TLS.ML

--- a/src/HOLCF/IOA/meta_theory/TLS.ML	Mon Jun 22 17:12:27 1998 +0200
+++ b/src/HOLCF/IOA/meta_theory/TLS.ML	Mon Jun 22 17:13:09 1998 +0200
@@ -17,7 +17,7 @@
 (*                                 ex2seqC                          *)
 (* ---------------------------------------------------------------- *)
 
-goal thy "ex2seqC  = (LAM ex. (%s. case ex of \
+Goal "ex2seqC  = (LAM ex. (%s. case ex of \
 \      nil =>  (s,None,s)>>nil   \
 \    | x##xs => (flift1 (%pr. \
 \                (s,Some (fst pr), snd pr)>> (ex2seqC`xs) (snd pr))  \
@@ -30,17 +30,17 @@
 by (simp_tac (simpset() addsimps [flift1_def]) 1);
 qed"ex2seqC_unfold";
 
-goal thy "(ex2seqC `UU) s=UU";
+Goal "(ex2seqC `UU) s=UU";
 by (stac ex2seqC_unfold 1);
 by (Simp_tac 1);
 qed"ex2seqC_UU";
 
-goal thy "(ex2seqC `nil) s = (s,None,s)>>nil";
+Goal "(ex2seqC `nil) s = (s,None,s)>>nil";
 by (stac ex2seqC_unfold 1);
 by (Simp_tac 1);
 qed"ex2seqC_nil";
 
-goal thy "(ex2seqC `((a,t)>>xs)) s = \
+Goal "(ex2seqC `((a,t)>>xs)) s = \
 \          (s,Some a,t)>> ((ex2seqC`xs) t)";
 by (rtac trans 1);
 by (stac ex2seqC_unfold 1);
@@ -51,15 +51,15 @@
 Addsimps [ex2seqC_UU,ex2seqC_nil,ex2seqC_cons];
 
 
-goal thy "ex2seq (s, UU) = UU";
+Goal "ex2seq (s, UU) = UU";
 by (simp_tac (simpset() addsimps [ex2seq_def]) 1);
 qed"ex2seq_UU";
 
-goal thy "ex2seq (s, nil) = (s,None,s)>>nil";
+Goal "ex2seq (s, nil) = (s,None,s)>>nil";
 by (simp_tac (simpset() addsimps [ex2seq_def]) 1);
 qed"ex2seq_nil";
 
-goal thy "ex2seq (s, (a,t)>>ex) = (s,Some a,t) >> ex2seq (t, ex)";
+Goal "ex2seq (s, (a,t)>>ex) = (s,Some a,t) >> ex2seq (t, ex)";
 by (simp_tac (simpset() addsimps [ex2seq_def]) 1);
 qed"ex2seq_cons";
 
@@ -69,17 +69,17 @@
 
 
 (* FIX: Not true for UU, as ex2seq is defined continously !!!!! *)
-goal thy "ex2seq exec ~= UU & ex2seq exec ~= nil";
+Goal "ex2seq exec ~= UU & ex2seq exec ~= nil";
 
 
-goal thy "ex |== [] P .--> P";
+Goal "ex |== [] P .--> P";
 
 
 (* ----------------------------------------------------------- *)
 (*           Interface TL -- TLS                               *)
 (* ---------------------------------------------------------- *)
 
-goalw thy [Init_def,Next_def,temp_sat_def,satisfies_def,IMPLIES_def,AND_def]
+Goalw [Init_def,Next_def,temp_sat_def,satisfies_def,IMPLIES_def,AND_def]
  "!! s. (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))))";