tidied
authorpaulson
Fri Jan 29 16:23:56 1999 +0100 (1999-01-29)
changeset 6161bc2a76ce1ea3
parent 6160 32c0b8f57bb7
child 6162 484adda70b65
tidied
src/HOL/UNITY/Lift.ML
src/HOLCF/IOA/Storage/Correctness.ML
src/HOLCF/IOA/meta_theory/Abstraction.ML
src/HOLCF/IOA/meta_theory/Asig.ML
src/HOLCF/IOA/meta_theory/Automata.ML
src/HOLCF/IOA/meta_theory/CompoScheds.ML
src/HOLCF/IOA/meta_theory/CompoTraces.ML
src/HOLCF/IOA/meta_theory/Compositionality.ML
src/HOLCF/IOA/meta_theory/Deadlock.ML
src/HOLCF/IOA/meta_theory/LiveIOA.ML
src/HOLCF/IOA/meta_theory/RefCorrectness.ML
src/HOLCF/IOA/meta_theory/RefMappings.ML
src/HOLCF/IOA/meta_theory/Seq.ML
src/HOLCF/IOA/meta_theory/Sequence.ML
src/HOLCF/IOA/meta_theory/ShortExecutions.ML
src/HOLCF/IOA/meta_theory/SimCorrectness.ML
src/HOLCF/IOA/meta_theory/TL.ML
src/HOLCF/IOA/meta_theory/TLS.ML
     1.1 --- a/src/HOL/UNITY/Lift.ML	Thu Jan 28 18:28:06 1999 +0100
     1.2 +++ b/src/HOL/UNITY/Lift.ML	Fri Jan 29 16:23:56 1999 +0100
     1.3 @@ -37,7 +37,6 @@
     1.4  (*The order in which they are applied seems to be critical...*)
     1.5  val mov_metrics = [mov_metric2, mov_metric3, mov_metric1, mov_metric4];
     1.6  
     1.7 -
     1.8  val metric_simps = [metric_def, vimage_def];
     1.9  
    1.10  
    1.11 @@ -109,7 +108,7 @@
    1.12  by (constrains_tac 1);
    1.13  by (ALLGOALS Clarify_tac);
    1.14  by (REPEAT_FIRST distinct_tac);
    1.15 -by (ALLGOALS (asm_simp_tac (simpset() addsimps [zle_imp_zle_zadd])));
    1.16 +by Auto_tac;
    1.17  qed "bounded";
    1.18  
    1.19  
    1.20 @@ -246,8 +245,6 @@
    1.21  by Auto_tac;
    1.22  by (REPEAT_FIRST (eresolve_tac mov_metrics));
    1.23  by (ALLGOALS (asm_simp_tac (simpset() addsimps metric_simps @ zcompare_rls)));
    1.24 -(** LEVEL 5 **)
    1.25 -by (dres_inst_tac [("w1","Min")] (zle_iff_zadd RS iffD1) 1);
    1.26  by (Blast_tac 1);
    1.27  qed "E_thm16a";
    1.28  
    1.29 @@ -260,8 +257,6 @@
    1.30  by Auto_tac;
    1.31  by (REPEAT_FIRST (eresolve_tac mov_metrics));
    1.32  by (ALLGOALS (asm_simp_tac (simpset() addsimps metric_simps @ zcompare_rls)));
    1.33 -(** LEVEL 5 **)
    1.34 -by (dres_inst_tac [("z1","Max")] (zle_iff_zadd RS iffD1) 1);
    1.35  by (Blast_tac 1);
    1.36  qed "E_thm16b";
    1.37  
     2.1 --- a/src/HOLCF/IOA/Storage/Correctness.ML	Thu Jan 28 18:28:06 1999 +0100
     2.2 +++ b/src/HOLCF/IOA/Storage/Correctness.ML	Fri Jan 29 16:23:56 1999 +0100
     2.3 @@ -28,7 +28,7 @@
     2.4  (* ---------------- main-part ------------------- *)
     2.5  
     2.6  by (REPEAT (rtac allI 1));
     2.7 -br imp_conj_lemma 1;
     2.8 +by (rtac imp_conj_lemma 1);
     2.9  ren "k b used c k' b' a" 1;
    2.10  by (induct_tac "a" 1);
    2.11  by (ALLGOALS (simp_tac (simpset() addsimps [sim_relation_def,
    2.12 @@ -37,13 +37,13 @@
    2.13  (* NEW *)
    2.14  by (res_inst_tac [("x","(used,True)")] exI 1);
    2.15  by (Asm_full_simp_tac 1);
    2.16 -br transition_is_ex 1;
    2.17 +by (rtac transition_is_ex 1);
    2.18  by (simp_tac (simpset() addsimps [
    2.19        Spec.ioa_def,Spec.trans_def,trans_of_def])1);
    2.20  (* LOC *)
    2.21  by (res_inst_tac [("x","(used Un {k},False)")] exI 1);
    2.22  by (Asm_full_simp_tac 1);
    2.23 -br transition_is_ex 1;
    2.24 +by (rtac transition_is_ex 1);
    2.25  by (simp_tac (simpset() addsimps [
    2.26        Spec.ioa_def,Spec.trans_def,trans_of_def])1);
    2.27  by (Fast_tac 1);
    2.28 @@ -51,8 +51,8 @@
    2.29  by (res_inst_tac [("x","(used - {nat},c)")] exI 1);
    2.30  by (Asm_full_simp_tac 1);
    2.31  by (SELECT_GOAL (safe_tac set_cs) 1);
    2.32 -auto();
    2.33 -br transition_is_ex 1;
    2.34 +by Auto_tac;
    2.35 +by (rtac transition_is_ex 1);
    2.36  by (simp_tac (simpset() addsimps [
    2.37        Spec.ioa_def,Spec.trans_def,trans_of_def])1);
    2.38  qed"issimulation";
    2.39 @@ -61,14 +61,14 @@
    2.40  
    2.41  Goalw [ioa_implements_def] 
    2.42  "impl_ioa =<| spec_ioa";
    2.43 -br conjI 1;
    2.44 +by (rtac conjI 1);
    2.45  by (simp_tac (simpset() addsimps [Impl.sig_def,Spec.sig_def,
    2.46      Impl.ioa_def,Spec.ioa_def, asig_outputs_def,asig_of_def,
    2.47      asig_inputs_def]) 1);
    2.48 -br trace_inclusion_for_simulations 1;
    2.49 +by (rtac trace_inclusion_for_simulations 1);
    2.50  by (simp_tac (simpset() addsimps [Impl.sig_def,Spec.sig_def,
    2.51      Impl.ioa_def,Spec.ioa_def, externals_def,asig_outputs_def,asig_of_def,
    2.52      asig_inputs_def]) 1);
    2.53 -br issimulation 1;
    2.54 +by (rtac issimulation 1);
    2.55  qed"implementation";
    2.56  
     3.1 --- a/src/HOLCF/IOA/meta_theory/Abstraction.ML	Thu Jan 28 18:28:06 1999 +0100
     3.2 +++ b/src/HOLCF/IOA/meta_theory/Abstraction.ML	Fri Jan 29 16:23:56 1999 +0100
     3.3 @@ -57,7 +57,7 @@
     3.4  
     3.5  
     3.6  Goalw [cex_abs_def]
     3.7 - "!!h.[| is_abstraction h C A |] ==>\
     3.8 + "[| is_abstraction h C A |] ==>\
     3.9  \ !s. reachable C s & is_exec_frag C (s,xs) \
    3.10  \ --> is_exec_frag A (cex_abs h (s,xs))"; 
    3.11  
    3.12 @@ -72,7 +72,7 @@
    3.13  qed_spec_mp"exec_frag_abstraction";
    3.14  
    3.15  
    3.16 -Goal "!!A. is_abstraction h C A ==> weakeningIOA A C h";
    3.17 +Goal "is_abstraction h C A ==> weakeningIOA A C h";
    3.18  by (asm_full_simp_tac (simpset() addsimps [weakeningIOA_def])1);
    3.19  by Auto_tac;
    3.20  by (asm_full_simp_tac (simpset() addsimps [executions_def]) 1);
    3.21 @@ -85,7 +85,7 @@
    3.22  qed"abs_is_weakening";
    3.23  
    3.24  
    3.25 -Goal "!!A. [|is_abstraction h C A; validIOA A Q; temp_strengthening Q P h |] \
    3.26 +Goal "[|is_abstraction h C A; validIOA A Q; temp_strengthening Q P h |] \
    3.27  \         ==> validIOA C P";
    3.28  by (dtac abs_is_weakening 1);
    3.29  by (asm_full_simp_tac (simpset() addsimps [weakeningIOA_def, 
    3.30 @@ -117,7 +117,7 @@
    3.31  
    3.32  
    3.33  Goalw [is_live_abstraction_def]
    3.34 -   "!!A. [|is_live_abstraction h (C,L) (A,M); \
    3.35 +   "[|is_live_abstraction h (C,L) (A,M); \
    3.36  \         validLIOA (A,M) Q;  temp_strengthening Q P h |] \
    3.37  \         ==> validLIOA (C,L) P";
    3.38  by Auto_tac;
    3.39 @@ -130,7 +130,7 @@
    3.40  
    3.41  
    3.42  Goalw [is_live_abstraction_def]
    3.43 -   "!!A. [|is_live_abstraction h (C,L) (A,M); \
    3.44 +   "[|is_live_abstraction h (C,L) (A,M); \
    3.45  \         validLIOA (A,M) (H1 .--> Q);  temp_strengthening Q P h; \
    3.46  \         temp_weakening H1 H2 h; validLIOA (C,L) H2 |] \
    3.47  \         ==> validLIOA (C,L) P";
    3.48 @@ -151,14 +151,14 @@
    3.49  
    3.50  
    3.51  Goalw [is_abstraction_def,is_ref_map_def] 
    3.52 -"!! h. is_abstraction h C A ==> is_ref_map h C A";
    3.53 +"is_abstraction h C A ==> is_ref_map h C A";
    3.54  by (safe_tac set_cs);
    3.55  by (res_inst_tac[("x","(a,h t)>>nil")] exI 1);
    3.56  by (asm_full_simp_tac (simpset() addsimps [move_def])1);
    3.57  qed"abstraction_is_ref_map";
    3.58  
    3.59  
    3.60 -Goal "!! h. [| inp(C)=inp(A); out(C)=out(A); \
    3.61 +Goal "[| inp(C)=inp(A); out(C)=out(A); \
    3.62  \                  is_abstraction h C A |] \
    3.63  \               ==> C =<| A";
    3.64  by (asm_full_simp_tac (simpset() addsimps [ioa_implements_def]) 1);
    3.65 @@ -179,7 +179,7 @@
    3.66  (* Reduces to Filter (Map fst x) = Filter (Map fst (Map (%(a,t). (a,x)) x),
    3.67     that is to special Map Lemma *)
    3.68  Goalw [cex_abs_def,mk_trace_def,filter_act_def]
    3.69 -  "!! f. ext C = ext A \
    3.70 +  "ext C = ext A \
    3.71  \        ==> mk_trace C`xs = mk_trace A`(snd (cex_abs f (s,xs)))";
    3.72  by (Asm_full_simp_tac 1);
    3.73  by (pair_induct_tac "xs" [] 1);
    3.74 @@ -190,7 +190,7 @@
    3.75     is_live_abstraction includes temp_strengthening which is necessarily based
    3.76     on cex_abs and not on corresp_ex. Thus, the proof is redoone in a more specific
    3.77     way for cex_abs *)
    3.78 -Goal "!! h. [| inp(C)=inp(A); out(C)=out(A); \
    3.79 +Goal "[| inp(C)=inp(A); out(C)=out(A); \
    3.80  \                  is_live_abstraction h (C,M) (A,L) |] \
    3.81  \               ==> live_implements (C,M) (A,L)";
    3.82  
    3.83 @@ -223,7 +223,7 @@
    3.84  (* FIX: NAch Traces.ML bringen *)
    3.85  
    3.86  Goalw [ioa_implements_def] 
    3.87 -"!! A. [| A =<| B; B =<| C|] ==> A =<| C"; 
    3.88 +"[| A =<| B; B =<| C|] ==> A =<| C"; 
    3.89  by Auto_tac;
    3.90  qed"implements_trans";
    3.91  
    3.92 @@ -234,7 +234,7 @@
    3.93  (*                Abstraction Rules for Automata                    *)
    3.94  (* ---------------------------------------------------------------- *)
    3.95  
    3.96 -Goal "!! C. [| inp(C)=inp(A); out(C)=out(A); \
    3.97 +Goal "[| inp(C)=inp(A); out(C)=out(A); \
    3.98  \                  inp(Q)=inp(P); out(Q)=out(P); \
    3.99  \                  is_abstraction h1 C A; \
   3.100  \                  A =<| Q ; \
   3.101 @@ -250,7 +250,7 @@
   3.102  qed"AbsRuleA1";
   3.103  
   3.104  
   3.105 -Goal "!! C. [| inp(C)=inp(A); out(C)=out(A); \
   3.106 +Goal "[| inp(C)=inp(A); out(C)=out(A); \
   3.107  \                  inp(Q)=inp(P); out(Q)=out(P); \
   3.108  \                  is_live_abstraction h1 (C,LC) (A,LA); \
   3.109  \                  live_implements (A,LA) (Q,LQ) ; \
   3.110 @@ -276,28 +276,28 @@
   3.111  (* ---------------------------------------------------------------- *)
   3.112  
   3.113  Goalw [temp_strengthening_def]
   3.114 -"!! h. [| temp_strengthening P1 Q1 h; \
   3.115 +"[| temp_strengthening P1 Q1 h; \
   3.116  \         temp_strengthening P2 Q2 h |] \
   3.117  \      ==> temp_strengthening (P1 .& P2) (Q1 .& Q2) h";
   3.118  by Auto_tac;
   3.119  qed"strength_AND";
   3.120  
   3.121  Goalw [temp_strengthening_def]
   3.122 -"!! h. [| temp_strengthening P1 Q1 h; \
   3.123 +"[| temp_strengthening P1 Q1 h; \
   3.124  \         temp_strengthening P2 Q2 h |] \
   3.125  \      ==> temp_strengthening (P1 .| P2) (Q1 .| Q2) h";
   3.126  by Auto_tac;
   3.127  qed"strength_OR";
   3.128  
   3.129  Goalw [temp_strengthening_def]
   3.130 -"!! h. [| temp_weakening P Q h |] \
   3.131 +"[| temp_weakening P Q h |] \
   3.132  \      ==> temp_strengthening (.~ P) (.~ Q) h";
   3.133  by (asm_full_simp_tac (simpset() addsimps [temp_weakening_def2])1);
   3.134  by Auto_tac;
   3.135  qed"strength_NOT";
   3.136  
   3.137  Goalw [temp_strengthening_def]
   3.138 -"!! h. [| temp_weakening P1 Q1 h; \
   3.139 +"[| temp_weakening P1 Q1 h; \
   3.140  \         temp_strengthening P2 Q2 h |] \
   3.141  \      ==> temp_strengthening (P1 .--> P2) (Q1 .--> Q2) h";
   3.142  by (asm_full_simp_tac (simpset() addsimps [temp_weakening_def2])1);
   3.143 @@ -310,28 +310,28 @@
   3.144  (* ---------------------------------------------------------------- *)
   3.145  
   3.146  Goal
   3.147 -"!! h. [| temp_weakening P1 Q1 h; \
   3.148 +"[| temp_weakening P1 Q1 h; \
   3.149  \         temp_weakening P2 Q2 h |] \
   3.150  \      ==> temp_weakening (P1 .& P2) (Q1 .& Q2) h";
   3.151  by (asm_full_simp_tac (simpset() addsimps [temp_weakening_def2])1);
   3.152  qed"weak_AND";
   3.153  
   3.154  Goal 
   3.155 -"!! h. [| temp_weakening P1 Q1 h; \
   3.156 +"[| temp_weakening P1 Q1 h; \
   3.157  \         temp_weakening P2 Q2 h |] \
   3.158  \      ==> temp_weakening (P1 .| P2) (Q1 .| Q2) h";
   3.159  by (asm_full_simp_tac (simpset() addsimps [temp_weakening_def2])1);
   3.160  qed"weak_OR";
   3.161  
   3.162  Goalw [temp_strengthening_def]
   3.163 -"!! h. [| temp_strengthening P Q h |] \
   3.164 +"[| temp_strengthening P Q h |] \
   3.165  \      ==> temp_weakening (.~ P) (.~ Q) h";
   3.166  by (asm_full_simp_tac (simpset() addsimps [temp_weakening_def2])1);
   3.167  by Auto_tac;
   3.168  qed"weak_NOT";
   3.169  
   3.170  Goalw [temp_strengthening_def]
   3.171 -"!! h. [| temp_strengthening P1 Q1 h; \
   3.172 +"[| temp_strengthening P1 Q1 h; \
   3.173  \         temp_weakening P2 Q2 h |] \
   3.174  \      ==> temp_weakening (P1 .--> P2) (Q1 .--> Q2) h";
   3.175  by (asm_full_simp_tac (simpset() addsimps [temp_weakening_def2])1);
   3.176 @@ -373,7 +373,7 @@
   3.177  (* important property of ex2seq: can be shiftet, as defined "pointwise" *)
   3.178  
   3.179  Goalw [tsuffix_def,suffix_def]
   3.180 -"!!s. tsuffix s (ex2seq ex) ==> ? ex'. s = (ex2seq ex')";
   3.181 +"tsuffix s (ex2seq ex) ==> ? ex'. s = (ex2seq ex')";
   3.182  by Auto_tac;
   3.183  by (dtac ex2seqConc 1);
   3.184  by Auto_tac;
   3.185 @@ -395,7 +395,7 @@
   3.186    properties carry over *)
   3.187  
   3.188  Goalw [tsuffix_def,suffix_def,cex_absSeq_def]
   3.189 -"!! s. tsuffix s t ==> tsuffix (cex_absSeq h s) (cex_absSeq h t)";
   3.190 +"tsuffix s t ==> tsuffix (cex_absSeq h s) (cex_absSeq h t)";
   3.191  by Auto_tac;
   3.192  by (asm_full_simp_tac (simpset() addsimps [Mapnil])1);
   3.193  by (asm_full_simp_tac (simpset() addsimps [MapUU])1);
   3.194 @@ -406,7 +406,7 @@
   3.195  
   3.196  Goalw [temp_strengthening_def,state_strengthening_def, temp_sat_def,
   3.197  satisfies_def,Box_def]
   3.198 -"!! h. [| temp_strengthening P Q h |]\
   3.199 +"[| temp_strengthening P Q h |]\
   3.200  \      ==> temp_strengthening ([] P) ([] Q) h";
   3.201  by (clarify_tac set_cs 1);
   3.202  by (forward_tac [ex2seq_tsuffix] 1);
   3.203 @@ -420,7 +420,7 @@
   3.204  
   3.205  Goalw [temp_strengthening_def,state_strengthening_def,
   3.206  temp_sat_def,satisfies_def,Init_def,unlift_def]
   3.207 -"!! h. [| state_strengthening P Q h |]\
   3.208 +"[| state_strengthening P Q h |]\
   3.209  \      ==> temp_strengthening (Init P) (Init Q) h";
   3.210  by (safe_tac set_cs);
   3.211  by (pair_tac "ex" 1);
   3.212 @@ -464,7 +464,7 @@
   3.213  
   3.214  (* important property of ex2seq: can be shiftet, as defined "pointwise" *)
   3.215  
   3.216 -Goal "!!ex. [| (snd ex)~=UU ; (snd ex)~=nil |] ==> (? ex'. TL`(ex2seq ex) = ex2seq ex')";
   3.217 +Goal "[| (snd ex)~=UU ; (snd ex)~=nil |] ==> (? ex'. TL`(ex2seq ex) = ex2seq ex')";
   3.218  by (pair_tac "ex" 1);
   3.219  by (Seq_case_simp_tac "y" 1);
   3.220  by (pair_tac "a" 1);
   3.221 @@ -483,7 +483,7 @@
   3.222  
   3.223  Goalw [temp_strengthening_def,state_strengthening_def,
   3.224  temp_sat_def, satisfies_def,Next_def]
   3.225 -"!! h. [| temp_strengthening P Q h |]\
   3.226 +"[| temp_strengthening P Q h |]\
   3.227  \      ==> temp_strengthening (Next P) (Next Q) h";
   3.228  by (Asm_full_simp_tac 1);
   3.229  by (safe_tac set_cs);
   3.230 @@ -494,7 +494,7 @@
   3.231  (* cons case *)
   3.232  by (asm_full_simp_tac (simpset() addsimps [TL_ex2seq_nil,TL_ex2seq_UU,
   3.233          ex2seq_abs_cex,cex_absSeq_TL RS sym, ex2seqnilTL])1);
   3.234 -be conjE 1;
   3.235 +by (etac conjE 1);
   3.236  by (dtac TLex2seq 1);
   3.237  by (assume_tac 1);
   3.238  by Auto_tac;
   3.239 @@ -508,7 +508,7 @@
   3.240  
   3.241  
   3.242  Goal 
   3.243 -"!! h. [| state_weakening P Q h |]\
   3.244 +"[| state_weakening P Q h |]\
   3.245  \      ==> temp_weakening (Init P) (Init Q) h";
   3.246  by (asm_full_simp_tac (simpset() addsimps [temp_weakening_def2,
   3.247        state_weakening_def2, temp_sat_def,satisfies_def,Init_def,unlift_def])1);
   3.248 @@ -525,7 +525,7 @@
   3.249  
   3.250  
   3.251  Goalw [Diamond_def]
   3.252 -"!! h. [| temp_strengthening P Q h |]\
   3.253 +"[| temp_strengthening P Q h |]\
   3.254  \      ==> temp_strengthening (<> P) (<> Q) h";
   3.255  by (rtac strength_NOT 1);
   3.256  by (rtac weak_Box 1);
   3.257 @@ -533,7 +533,7 @@
   3.258  qed"strength_Diamond";
   3.259  
   3.260  Goalw [Leadsto_def]
   3.261 -"!! h. [| temp_weakening P1 P2 h;\
   3.262 +"[| temp_weakening P1 P2 h;\
   3.263  \         temp_strengthening Q1 Q2 h |]\
   3.264  \      ==> temp_strengthening (P1 ~> Q1) (P2 ~> Q2) h";
   3.265  by (rtac strength_Box 1);
   3.266 @@ -548,7 +548,7 @@
   3.267  
   3.268  
   3.269  Goalw [Diamond_def]
   3.270 -"!! h. [| temp_weakening P Q h |]\
   3.271 +"[| temp_weakening P Q h |]\
   3.272  \      ==> temp_weakening (<> P) (<> Q) h";
   3.273  by (rtac weak_NOT 1);
   3.274  by (rtac strength_Box 1);
   3.275 @@ -556,7 +556,7 @@
   3.276  qed"weak_Diamond";
   3.277  
   3.278  Goalw [Leadsto_def]
   3.279 -"!! h. [| temp_strengthening P1 P2 h;\
   3.280 +"[| temp_strengthening P1 P2 h;\
   3.281  \         temp_weakening Q1 Q2 h |]\
   3.282  \      ==> temp_weakening (P1 ~> Q1) (P2 ~> Q2) h";
   3.283  by (rtac weak_Box 1);
     4.1 --- a/src/HOLCF/IOA/meta_theory/Asig.ML	Thu Jan 28 18:28:06 1999 +0100
     4.2 +++ b/src/HOLCF/IOA/meta_theory/Asig.ML	Fri Jan 29 16:23:56 1999 +0100
     4.3 @@ -6,8 +6,6 @@
     4.4  Action signatures
     4.5  *)
     4.6  
     4.7 -open Asig;
     4.8 -
     4.9  val asig_projections = [asig_inputs_def, asig_outputs_def, asig_internals_def];
    4.10  
    4.11  Goal
    4.12 @@ -17,23 +15,23 @@
    4.13    by (simp_tac (simpset() addsimps asig_projections) 1);
    4.14  qed "asig_triple_proj";
    4.15  
    4.16 -Goal "!!a.[| a~:internals(S) ;a~:externals(S)|] ==> a~:actions(S)";
    4.17 +Goal "[| a~:internals(S) ;a~:externals(S)|] ==> a~:actions(S)";
    4.18  by (asm_full_simp_tac (simpset() addsimps [externals_def,actions_def]) 1);
    4.19  qed"int_and_ext_is_act";
    4.20  
    4.21 -Goal "!!a.[|a:externals(S)|] ==> a:actions(S)";
    4.22 +Goal "[|a:externals(S)|] ==> a:actions(S)";
    4.23  by (asm_full_simp_tac (simpset() addsimps [externals_def,actions_def]) 1);
    4.24  qed"ext_is_act";
    4.25  
    4.26 -Goal "!!a.[|a:internals S|] ==> a:actions S";
    4.27 +Goal "[|a:internals S|] ==> a:actions S";
    4.28  by (asm_full_simp_tac (simpset() addsimps [asig_internals_def,actions_def]) 1);
    4.29  qed"int_is_act";
    4.30  
    4.31 -Goal "!!a.[|a:inputs S|] ==> a:actions S";
    4.32 +Goal "[|a:inputs S|] ==> a:actions S";
    4.33  by (asm_full_simp_tac (simpset() addsimps [asig_inputs_def,actions_def]) 1);
    4.34  qed"inp_is_act";
    4.35  
    4.36 -Goal "!!a.[|a:outputs S|] ==> a:actions S";
    4.37 +Goal "[|a:outputs S|] ==> a:actions S";
    4.38  by (asm_full_simp_tac (simpset() addsimps [asig_outputs_def,actions_def]) 1);
    4.39  qed"out_is_act";
    4.40  
    4.41 @@ -41,19 +39,19 @@
    4.42  by (fast_tac (claset() addSIs [ext_is_act]) 1 );
    4.43  qed"ext_and_act";
    4.44   
    4.45 -Goal "!!S. [|is_asig S;x: actions S|] ==> (x~:externals S) = (x: internals S)";
    4.46 +Goal "[|is_asig S;x: actions S|] ==> (x~:externals S) = (x: internals S)";
    4.47  by (asm_full_simp_tac (simpset() addsimps [actions_def,is_asig_def,externals_def]) 1);
    4.48 -by (best_tac (set_cs addEs [equalityCE]) 1);
    4.49 +by (Blast_tac 1);
    4.50  qed"not_ext_is_int";
    4.51  
    4.52 -Goal "!!S. is_asig S ==> (x~:externals S) = (x: internals S | x~:actions S)";
    4.53 +Goal "is_asig S ==> (x~:externals S) = (x: internals S | x~:actions S)";
    4.54  by (asm_full_simp_tac (simpset() addsimps [actions_def,is_asig_def,externals_def]) 1);
    4.55 -by (best_tac (set_cs addEs [equalityCE]) 1);
    4.56 +by (Blast_tac 1);
    4.57  qed"not_ext_is_int_or_not_act";
    4.58  
    4.59  Goalw  [externals_def,actions_def,is_asig_def]
    4.60 - "!! x. [| is_asig (S); x:internals S |] ==> x~:externals S";
    4.61 + "[| is_asig (S); x:internals S |] ==> x~:externals S";
    4.62  by (Asm_full_simp_tac 1);
    4.63 -by (best_tac (set_cs addEs [equalityCE]) 1);
    4.64 +by (Blast_tac 1);
    4.65  qed"int_is_not_ext";
    4.66  
     5.1 --- a/src/HOLCF/IOA/meta_theory/Automata.ML	Thu Jan 28 18:28:06 1999 +0100
     5.2 +++ b/src/HOLCF/IOA/meta_theory/Automata.ML	Fri Jan 29 16:23:56 1999 +0100
     5.3 @@ -9,12 +9,9 @@
     5.4  (* this modification of the simpset is local to this file *)
     5.5  Delsimps [split_paired_Ex];
     5.6  
     5.7 -
     5.8 -open reachable;
     5.9 -
    5.10  val ioa_projections = [asig_of_def, starts_of_def, trans_of_def,wfair_of_def,sfair_of_def];
    5.11  
    5.12 -(* ----------------------------------------------------------------------------------- *)
    5.13 +(* ------------------------------------------------------------------------- *)
    5.14  
    5.15  section "asig_of, starts_of, trans_of";
    5.16  
    5.17 @@ -29,7 +26,7 @@
    5.18  qed "ioa_triple_proj";
    5.19  
    5.20  Goalw [is_trans_of_def,actions_def, is_asig_def]
    5.21 -  "!!A. [| is_trans_of A; (s1,a,s2):trans_of(A) |] ==> a:act A";
    5.22 +  "[| is_trans_of A; (s1,a,s2):trans_of(A) |] ==> a:act A";
    5.23    by (REPEAT(etac conjE 1));
    5.24    by (EVERY1[etac allE, etac impE, atac]);
    5.25    by (Asm_full_simp_tac 1);
    5.26 @@ -55,7 +52,7 @@
    5.27  qed "trans_of_par";
    5.28  
    5.29  
    5.30 -(* ----------------------------------------------------------------------------------- *)
    5.31 +(* ------------------------------------------------------------------------- *)
    5.32  
    5.33  section "actions and par";
    5.34  
    5.35 @@ -107,7 +104,7 @@
    5.36        asig_inputs_def,asig_outputs_def,asig_internals_def,Un_def,set_diff_def]) 1);
    5.37  qed"internals_of_par";
    5.38  
    5.39 -(* ---------------------------------------------------------------------------------- *)
    5.40 +(* ------------------------------------------------------------------------ *)
    5.41  
    5.42  section "actions and compatibility"; 
    5.43  
    5.44 @@ -117,50 +114,50 @@
    5.45  qed"compat_commute";
    5.46  
    5.47  Goalw [externals_def,actions_def,compatible_def]
    5.48 - "!! a. [| compatible A1 A2; a:ext A1|] ==> a~:int A2";
    5.49 + "[| compatible A1 A2; a:ext A1|] ==> a~:int A2";
    5.50  by (Asm_full_simp_tac 1);
    5.51 -by (best_tac (set_cs addEs [equalityCE]) 1);
    5.52 +by (Blast_tac 1);
    5.53  qed"ext1_is_not_int2";
    5.54  
    5.55  (* just commuting the previous one: better commute compatible *)
    5.56  Goalw [externals_def,actions_def,compatible_def]
    5.57 - "!! a. [| compatible A2 A1 ; a:ext A1|] ==> a~:int A2";
    5.58 + "[| compatible A2 A1 ; a:ext A1|] ==> a~:int A2";
    5.59  by (Asm_full_simp_tac 1);
    5.60 -by (best_tac (set_cs addEs [equalityCE]) 1);
    5.61 +by (Blast_tac 1);
    5.62  qed"ext2_is_not_int1";
    5.63  
    5.64  bind_thm("ext1_ext2_is_not_act2",ext1_is_not_int2 RS int_and_ext_is_act);
    5.65  bind_thm("ext1_ext2_is_not_act1",ext2_is_not_int1 RS int_and_ext_is_act);
    5.66  
    5.67  Goalw  [externals_def,actions_def,compatible_def]
    5.68 - "!! x. [| compatible A B; x:int A |] ==> x~:ext B";
    5.69 + "[| compatible A B; x:int A |] ==> x~:ext B";
    5.70  by (Asm_full_simp_tac 1);
    5.71 -by (best_tac (set_cs addEs [equalityCE]) 1);
    5.72 +by (Blast_tac 1);
    5.73  qed"intA_is_not_extB";
    5.74  
    5.75  Goalw [externals_def,actions_def,compatible_def,is_asig_def,asig_of_def]
    5.76 -"!! a. [| compatible A B; a:int A |] ==> a ~: act B";
    5.77 +"[| compatible A B; a:int A |] ==> a ~: act B";
    5.78  by (Asm_full_simp_tac 1);
    5.79 -by (best_tac (set_cs addEs [equalityCE]) 1);
    5.80 +by (Blast_tac 1);
    5.81  qed"intA_is_not_actB";
    5.82  
    5.83  (* the only one that needs disjointness of outputs and of internals and _all_ acts *)
    5.84  Goalw [asig_outputs_def,asig_internals_def,actions_def,asig_inputs_def,
    5.85      compatible_def,is_asig_def,asig_of_def]
    5.86 -"!! a. [| compatible A B; a:out A ;a:act B|] ==> a : inp B";
    5.87 +"[| compatible A B; a:out A ;a:act B|] ==> a : inp B";
    5.88  by (Asm_full_simp_tac 1);
    5.89 -by (best_tac (set_cs addEs [equalityCE]) 1);
    5.90 +by (Blast_tac 1);
    5.91  qed"outAactB_is_inpB";
    5.92  
    5.93  (* needed for propagation of input_enabledness from A,B to A||B *)
    5.94  Goalw [asig_outputs_def,asig_internals_def,actions_def,asig_inputs_def,
    5.95      compatible_def,is_asig_def,asig_of_def]
    5.96 -"!! a. [| compatible A B; a:inp A ;a:act B|] ==> a : inp B | a: out B";
    5.97 +"[| compatible A B; a:inp A ;a:act B|] ==> a : inp B | a: out B";
    5.98  by (Asm_full_simp_tac 1);
    5.99 -by (best_tac (set_cs addEs [equalityCE]) 1);
   5.100 +by (Blast_tac 1);
   5.101  qed"inpAAactB_is_inpBoroutB";
   5.102  
   5.103 -(* ---------------------------------------------------------------------------------- *)
   5.104 +(* ------------------------------------------------------------------------- *)
   5.105  
   5.106  section "input_enabledness and par";  
   5.107  
   5.108 @@ -169,7 +166,7 @@
   5.109       1. inpAAactB_is_inpBoroutB ie. internals are really hidden.
   5.110       2. inputs_of_par: outputs are no longer inputs of par. This is important here *)
   5.111  Goalw [input_enabled_def] 
   5.112 -"!!A. [| compatible A B; input_enabled A; input_enabled B|] \
   5.113 +"[| compatible A B; input_enabled A; input_enabled B|] \
   5.114  \     ==> input_enabled (A||B)";
   5.115  by (asm_full_simp_tac (simpset()addsimps[Let_def,inputs_of_par,trans_of_par])1);
   5.116  by (safe_tac set_cs);
   5.117 @@ -232,7 +229,7 @@
   5.118  by (Asm_full_simp_tac 1);
   5.119  qed"input_enabled_par";
   5.120  
   5.121 -(* ---------------------------------------------------------------------------------- *)
   5.122 +(* ------------------------------------------------------------------------- *)
   5.123  
   5.124  section "invariants";
   5.125  
   5.126 @@ -252,21 +249,23 @@
   5.127  
   5.128  val [p1,p2] = goal thy
   5.129   "[| !!s. s : starts_of(A) ==> P(s); \
   5.130 -\   !!s t a. reachable A s ==> P(s) --> (s,a,t):trans_of(A) --> P(t) \
   5.131 +\    !!s t a. reachable A s ==> P(s) --> (s,a,t):trans_of(A) --> P(t) \
   5.132  \ |] ==> invariant A P";
   5.133    by (fast_tac (HOL_cs addSIs [invariantI] addSDs [p1,p2]) 1);
   5.134  qed "invariantI1";
   5.135  
   5.136 -val [p1,p2] = goalw thy [invariant_def]
   5.137 -"[| invariant A P; reachable A s |] ==> P(s)";
   5.138 -   br(p2 RS (p1 RS spec RS mp))1;
   5.139 +Goalw [invariant_def] "[| invariant A P; reachable A s |] ==> P(s)";
   5.140 +by (Blast_tac 1);   
   5.141  qed "invariantE";
   5.142  
   5.143 -(* ---------------------------------------------------------------------------------- *)
   5.144 +(* ------------------------------------------------------------------------- *)
   5.145  
   5.146  section "restrict";
   5.147  
   5.148  
   5.149 +val reachable_0 = reachable.reachable_0
   5.150 +and reachable_n = reachable.reachable_n;
   5.151 +
   5.152  Goal "starts_of(restrict ioa acts) = starts_of(ioa) &     \
   5.153  \         trans_of(restrict ioa acts) = trans_of(ioa)";
   5.154  by (simp_tac (simpset() addsimps ([restrict_def]@ioa_projections)) 1);
   5.155 @@ -300,18 +299,18 @@
   5.156    by (simp_tac (simpset() addsimps [cancel_restrict_a,cancel_restrict_b,acts_restrict]) 1);
   5.157  qed"cancel_restrict";
   5.158  
   5.159 -(* ---------------------------------------------------------------------------------- *)
   5.160 +(* ------------------------------------------------------------------------- *)
   5.161  
   5.162  section "rename";
   5.163  
   5.164  
   5.165  
   5.166 -Goal "!!f. s -a--(rename C f)-> t ==> (? x. Some(x) = f(a) & s -x--C-> t)";
   5.167 +Goal "s -a--(rename C f)-> t ==> (? x. Some(x) = f(a) & s -x--C-> t)";
   5.168  by (asm_full_simp_tac (simpset() addsimps [Let_def,rename_def,trans_of_def]) 1);
   5.169  qed"trans_rename";
   5.170  
   5.171  
   5.172 -Goal "!!s.[| reachable (rename C g) s |] ==> reachable C s";
   5.173 +Goal "[| reachable (rename C g) s |] ==> reachable C s";
   5.174  by (etac reachable.induct 1);
   5.175  by (rtac reachable_0 1);
   5.176  by (asm_full_simp_tac (simpset() addsimps [rename_def]@ioa_projections) 1);
   5.177 @@ -324,49 +323,49 @@
   5.178  
   5.179  
   5.180  
   5.181 -(* ---------------------------------------------------------------------------------- *)
   5.182 +(* ------------------------------------------------------------------------- *)
   5.183  
   5.184  section "trans_of(A||B)";
   5.185  
   5.186  
   5.187 -Goal "!!A.[|(s,a,t):trans_of (A||B); a:act A|] \
   5.188 +Goal "[|(s,a,t):trans_of (A||B); a:act A|] \
   5.189  \             ==> (fst s,a,fst t):trans_of A";
   5.190  by (asm_full_simp_tac (simpset() addsimps [Let_def,par_def,trans_of_def]) 1);
   5.191  qed"trans_A_proj";
   5.192  
   5.193 -Goal "!!A.[|(s,a,t):trans_of (A||B); a:act B|] \
   5.194 +Goal "[|(s,a,t):trans_of (A||B); a:act B|] \
   5.195  \             ==> (snd s,a,snd t):trans_of B";
   5.196  by (asm_full_simp_tac (simpset() addsimps [Let_def,par_def,trans_of_def]) 1);
   5.197  qed"trans_B_proj";
   5.198  
   5.199 -Goal "!!A.[|(s,a,t):trans_of (A||B); a~:act A|]\
   5.200 +Goal "[|(s,a,t):trans_of (A||B); a~:act A|]\
   5.201  \             ==> fst s = fst t";
   5.202  by (asm_full_simp_tac (simpset() addsimps [Let_def,par_def,trans_of_def]) 1);
   5.203  qed"trans_A_proj2";
   5.204  
   5.205 -Goal "!!A.[|(s,a,t):trans_of (A||B); a~:act B|]\
   5.206 +Goal "[|(s,a,t):trans_of (A||B); a~:act B|]\
   5.207  \             ==> snd s = snd t";
   5.208  by (asm_full_simp_tac (simpset() addsimps [Let_def,par_def,trans_of_def]) 1);
   5.209  qed"trans_B_proj2";
   5.210  
   5.211 -Goal "!!A.(s,a,t):trans_of (A||B) \
   5.212 +Goal "(s,a,t):trans_of (A||B) \
   5.213  \              ==> a :act A | a :act B";
   5.214  by (asm_full_simp_tac (simpset() addsimps [Let_def,par_def,trans_of_def]) 1);
   5.215  qed"trans_AB_proj";
   5.216  
   5.217 -Goal "!!A. [|a:act A;a:act B;\
   5.218 +Goal "[|a:act A;a:act B;\
   5.219  \      (fst s,a,fst t):trans_of A;(snd s,a,snd t):trans_of B|]\
   5.220  \  ==> (s,a,t):trans_of (A||B)";
   5.221  by (asm_full_simp_tac (simpset() addsimps [Let_def,par_def,trans_of_def]) 1);
   5.222  qed"trans_AB";
   5.223  
   5.224 -Goal "!!A. [|a:act A;a~:act B;\
   5.225 +Goal "[|a:act A;a~:act B;\
   5.226  \      (fst s,a,fst t):trans_of A;snd s=snd t|]\
   5.227  \  ==> (s,a,t):trans_of (A||B)";
   5.228  by (asm_full_simp_tac (simpset() addsimps [Let_def,par_def,trans_of_def]) 1);
   5.229  qed"trans_A_notB";
   5.230  
   5.231 -Goal "!!A. [|a~:act A;a:act B;\
   5.232 +Goal "[|a~:act A;a:act B;\
   5.233  \      (snd s,a,snd t):trans_of B;fst s=fst t|]\
   5.234  \  ==> (s,a,t):trans_of (A||B)";
   5.235  by (asm_full_simp_tac (simpset() addsimps [Let_def,par_def,trans_of_def]) 1);
   5.236 @@ -397,7 +396,7 @@
   5.237  qed "trans_of_par4";
   5.238  
   5.239  
   5.240 -(* ---------------------------------------------------------------------------------- *)
   5.241 +(* ------------------------------------------------------------------------- *)
   5.242  
   5.243  section "proof obligation generator for IOA requirements";  
   5.244  
   5.245 @@ -407,12 +406,12 @@
   5.246  qed"is_trans_of_par";
   5.247  
   5.248  Goalw [is_trans_of_def] 
   5.249 -"!!A. is_trans_of A ==> is_trans_of (restrict A acts)";
   5.250 +"is_trans_of A ==> is_trans_of (restrict A acts)";
   5.251  by (asm_simp_tac (simpset() addsimps [cancel_restrict,acts_restrict])1);
   5.252  qed"is_trans_of_restrict";
   5.253  
   5.254  Goalw [is_trans_of_def,restrict_def,restrict_asig_def] 
   5.255 -"!!A. is_trans_of A ==> is_trans_of (rename A f)";
   5.256 +"is_trans_of A ==> is_trans_of (rename A f)";
   5.257  by (asm_full_simp_tac
   5.258      (simpset() addsimps [Let_def,actions_def,trans_of_def, asig_internals_def,
   5.259  			 asig_outputs_def,asig_inputs_def,externals_def,
   5.260 @@ -420,31 +419,29 @@
   5.261  by (Blast_tac 1);
   5.262  qed"is_trans_of_rename";
   5.263  
   5.264 -Goal "!! A. [| is_asig_of A; is_asig_of B; compatible A B|]  \
   5.265 +Goal "[| is_asig_of A; is_asig_of B; compatible A B|]  \
   5.266  \         ==> is_asig_of (A||B)";
   5.267  by (asm_full_simp_tac (simpset() addsimps [is_asig_of_def,asig_of_par,
   5.268         asig_comp_def,compatible_def,asig_internals_def,asig_outputs_def,
   5.269       asig_inputs_def,actions_def,is_asig_def]) 1);
   5.270  by (asm_full_simp_tac (simpset() addsimps [asig_of_def]) 1);
   5.271  by Auto_tac;
   5.272 -by (REPEAT (best_tac (set_cs addEs [equalityCE]) 1));
   5.273  qed"is_asig_of_par";
   5.274  
   5.275  Goalw [is_asig_of_def,is_asig_def,asig_of_def,restrict_def,restrict_asig_def,
   5.276             asig_internals_def,asig_outputs_def,asig_inputs_def,externals_def,o_def] 
   5.277 -"!! A. is_asig_of A ==> is_asig_of (restrict A f)";
   5.278 +"is_asig_of A ==> is_asig_of (restrict A f)";
   5.279  by (Asm_full_simp_tac 1);
   5.280  by Auto_tac;
   5.281 -by (REPEAT (best_tac (set_cs addEs [equalityCE]) 1));
   5.282  qed"is_asig_of_restrict";
   5.283  
   5.284 -Goal "!! A. is_asig_of A ==> is_asig_of (rename A f)";
   5.285 +Goal "is_asig_of A ==> is_asig_of (rename A f)";
   5.286  by (asm_full_simp_tac (simpset() addsimps [is_asig_of_def,
   5.287       rename_def,rename_set_def,asig_internals_def,asig_outputs_def,
   5.288       asig_inputs_def,actions_def,is_asig_def,asig_of_def]) 1);
   5.289  by Auto_tac; 
   5.290  by   (ALLGOALS(dres_inst_tac [("s","Some ?x")] sym THEN' Asm_full_simp_tac));
   5.291 -by   (ALLGOALS(best_tac (set_cs addEs [equalityCE])));
   5.292 +by   (ALLGOALS(Blast_tac));
   5.293  qed"is_asig_of_rename";
   5.294  
   5.295  
   5.296 @@ -453,28 +450,26 @@
   5.297  
   5.298  
   5.299  Goalw [compatible_def]
   5.300 -"!! A. [|compatible A B; compatible A C |]==> compatible A (B||C)";
   5.301 +"[|compatible A B; compatible A C |]==> compatible A (B||C)";
   5.302  by (asm_full_simp_tac (simpset() addsimps [internals_of_par, 
   5.303     outputs_of_par,actions_of_par]) 1);
   5.304  by Auto_tac;
   5.305 -by (REPEAT (best_tac (set_cs addEs [equalityCE]) 1));
   5.306  qed"compatible_par";
   5.307  
   5.308  (*  better derive by previous one and compat_commute *)
   5.309  Goalw [compatible_def]
   5.310 -"!! A. [|compatible A C; compatible B C |]==> compatible (A||B) C";
   5.311 +"[|compatible A C; compatible B C |]==> compatible (A||B) C";
   5.312  by (asm_full_simp_tac (simpset() addsimps [internals_of_par, 
   5.313     outputs_of_par,actions_of_par]) 1);
   5.314  by Auto_tac;
   5.315 -by (REPEAT (best_tac (set_cs addEs [equalityCE]) 1));
   5.316  qed"compatible_par2";
   5.317  
   5.318  Goalw [compatible_def]
   5.319 -"!! A. [| compatible A B; (ext B - S) Int ext A = {}|] \
   5.320 +"[| compatible A B; (ext B - S) Int ext A = {}|] \
   5.321  \     ==> compatible A (restrict B S)";
   5.322  by (asm_full_simp_tac (simpset() addsimps [ioa_triple_proj,asig_triple_proj,
   5.323            externals_def,restrict_def,restrict_asig_def,actions_def]) 1);
   5.324 -by (auto_tac (claset() addEs [equalityCE],simpset()));
   5.325 +by Auto_tac;
   5.326  qed"compatible_restrict";
   5.327  
   5.328  
     6.1 --- a/src/HOLCF/IOA/meta_theory/CompoScheds.ML	Thu Jan 28 18:28:06 1999 +0100
     6.2 +++ b/src/HOLCF/IOA/meta_theory/CompoScheds.ML	Fri Jan 29 16:23:56 1999 +0100
     6.3 @@ -66,7 +66,7 @@
     6.4  by (Simp_tac 1);
     6.5  qed"mkex2_nil";
     6.6  
     6.7 -Goal "!!x.[| x:act A; x~:act B; HD`exA=Def a|] \
     6.8 +Goal "[| x:act A; x~:act B; HD`exA=Def a|] \
     6.9  \   ==> (mkex2 A B`(x>>sch)`exA`exB) s t =   \
    6.10  \       (x,snd a,t) >> (mkex2 A B`sch`(TL`exA)`exB) (snd a) t";
    6.11  by (rtac trans 1);
    6.12 @@ -75,7 +75,7 @@
    6.13  by (asm_full_simp_tac (simpset() addsimps [Cons_def]) 1);
    6.14  qed"mkex2_cons_1";
    6.15  
    6.16 -Goal "!!x.[| x~:act A; x:act B; HD`exB=Def b|] \
    6.17 +Goal "[| x~:act A; x:act B; HD`exB=Def b|] \
    6.18  \   ==> (mkex2 A B`(x>>sch)`exA`exB) s t = \
    6.19  \       (x,s,snd b) >> (mkex2 A B`sch`exA`(TL`exB)) s (snd b)";
    6.20  by (rtac trans 1);
    6.21 @@ -84,7 +84,7 @@
    6.22  by (asm_full_simp_tac (simpset() addsimps [Cons_def]) 1);
    6.23  qed"mkex2_cons_2";
    6.24  
    6.25 -Goal "!!x.[| x:act A; x:act B; HD`exA=Def a;HD`exB=Def b|] \
    6.26 +Goal "[| x:act A; x:act B; HD`exA=Def a;HD`exB=Def b|] \
    6.27  \   ==> (mkex2 A B`(x>>sch)`exA`exB) s t =  \
    6.28  \        (x,snd a,snd b) >> \
    6.29  \           (mkex2 A B`sch`(TL`exA)`(TL`exB)) (snd a) (snd b)";
    6.30 @@ -109,7 +109,7 @@
    6.31  by (simp_tac (simpset() addsimps [mkex_def]) 1);
    6.32  qed"mkex_nil";
    6.33  
    6.34 -Goal "!!x.[| x:act A; x~:act B |] \
    6.35 +Goal "[| x:act A; x~:act B |] \
    6.36  \   ==> mkex A B (x>>sch) (s,a>>exA) (t,exB)  =  \
    6.37  \       ((s,t), (x,snd a,t) >> snd (mkex A B sch (snd a,exA) (t,exB)))";
    6.38  by (simp_tac (simpset() addsimps [mkex_def]) 1);
    6.39 @@ -117,7 +117,7 @@
    6.40  by Auto_tac;
    6.41  qed"mkex_cons_1";
    6.42  
    6.43 -Goal "!!x.[| x~:act A; x:act B |] \
    6.44 +Goal "[| x~:act A; x:act B |] \
    6.45  \   ==> mkex A B (x>>sch) (s,exA) (t,b>>exB) =  \ 
    6.46  \       ((s,t), (x,s,snd b) >> snd (mkex A B sch (s,exA) (snd b,exB)))";
    6.47  by (simp_tac (simpset() addsimps [mkex_def]) 1);
    6.48 @@ -125,7 +125,7 @@
    6.49  by Auto_tac;
    6.50  qed"mkex_cons_2";
    6.51  
    6.52 -Goal "!!x.[| x:act A; x:act B |]  \
    6.53 +Goal "[| x:act A; x:act B |]  \
    6.54  \   ==>  mkex A B (x>>sch) (s,a>>exA) (t,b>>exB) = \
    6.55  \        ((s,t), (x,snd a,snd b) >> snd (mkex A B sch (snd a,exA) (snd b,exB)))";
    6.56  by (simp_tac (simpset() addsimps [mkex_def]) 1);
    6.57 @@ -277,7 +277,7 @@
    6.58  qed"stutterA_mkex";
    6.59  
    6.60  
    6.61 -Goal "!! sch.[|  \
    6.62 +Goal "[|  \
    6.63  \ Forall (%x. x:act (A||B)) sch ; \
    6.64  \ Filter (%a. a:act A)`sch << filter_act`(snd exA) ;\
    6.65  \ Filter (%a. a:act B)`sch << filter_act`(snd exB) |] \
    6.66 @@ -308,7 +308,7 @@
    6.67  qed"stutterB_mkex";
    6.68  
    6.69  
    6.70 -Goal "!! sch.[|  \
    6.71 +Goal "[|  \
    6.72  \ Forall (%x. x:act (A||B)) sch ; \
    6.73  \ Filter (%a. a:act A)`sch << filter_act`(snd exA) ;\
    6.74  \ Filter (%a. a:act B)`sch << filter_act`(snd exB) |] \
     7.1 --- a/src/HOLCF/IOA/meta_theory/CompoTraces.ML	Thu Jan 28 18:28:06 1999 +0100
     7.2 +++ b/src/HOLCF/IOA/meta_theory/CompoTraces.ML	Fri Jan 29 16:23:56 1999 +0100
     7.3 @@ -60,7 +60,7 @@
     7.4  by (Simp_tac 1);
     7.5  qed"mksch_nil";
     7.6  
     7.7 -Goal "!!x.[|x:act A;x~:act B|]  \
     7.8 +Goal "[|x:act A;x~:act B|]  \
     7.9  \   ==> mksch A B`(x>>tr)`schA`schB = \
    7.10  \         (Takewhile (%a. a:int A)`schA) \
    7.11  \         @@ (x>>(mksch A B`tr`(TL`(Dropwhile (%a. a:int A)`schA)) \
    7.12 @@ -71,7 +71,7 @@
    7.13  by (simp_tac (simpset() addsimps [Cons_def]) 1);
    7.14  qed"mksch_cons1";
    7.15  
    7.16 -Goal "!!x.[|x~:act A;x:act B|] \
    7.17 +Goal "[|x~:act A;x:act B|] \
    7.18  \   ==> mksch A B`(x>>tr)`schA`schB = \
    7.19  \        (Takewhile (%a. a:int B)`schB)  \
    7.20  \         @@ (x>>(mksch A B`tr`schA`(TL`(Dropwhile (%a. a:int B)`schB))  \
    7.21 @@ -82,7 +82,7 @@
    7.22  by (simp_tac (simpset() addsimps [Cons_def]) 1);
    7.23  qed"mksch_cons2";
    7.24  
    7.25 -Goal "!!x.[|x:act A;x:act B|] \
    7.26 +Goal "[|x:act A;x:act B|] \
    7.27  \   ==> mksch A B`(x>>tr)`schA`schB = \
    7.28  \            (Takewhile (%a. a:int A)`schA) \
    7.29  \         @@ ((Takewhile (%a. a:int B)`schB)  \
    7.30 @@ -199,7 +199,7 @@
    7.31  (* safe-tac makes too many case distinctions with this lemma in the next proof *)
    7.32  Delsimps [FiniteConc];
    7.33  
    7.34 -Goal "!! tr. [| Finite tr; is_asig(asig_of A); is_asig(asig_of B) |] ==> \
    7.35 +Goal "[| Finite tr; is_asig(asig_of A); is_asig(asig_of B) |] ==> \
    7.36  \   ! x y. Forall (%x. x:act A) x & Forall (%x. x:act B) y & \
    7.37  \          Filter (%a. a:ext A)`x = Filter (%a. a:act A)`tr & \
    7.38  \          Filter (%a. a:ext B)`y = Filter (%a. a:act B)`tr &\
    7.39 @@ -272,7 +272,7 @@
    7.40  (* otherwise subst_lemma2 does not fit exactly, just to avoid a subst_lemma3 *)
    7.41  Delsimps [FilterConc]; 
    7.42  
    7.43 -Goal " !!bs. [| Finite bs; is_asig(asig_of A); is_asig(asig_of B);compatible A B|] ==>  \
    7.44 +Goal " [| Finite bs; is_asig(asig_of A); is_asig(asig_of B);compatible A B|] ==>  \
    7.45  \! y. Forall (%x. x:act B) y & Forall (%x. x:act B & x~:act A) bs &\
    7.46  \    Filter (%a. a:ext B)`y = Filter (%a. a:act B)`(bs @@ z) \
    7.47  \    --> (? y1 y2.  (mksch A B`(bs @@ z)`x`y) = (y1 @@ (mksch A B`z`x`y2)) & \
    7.48 @@ -326,7 +326,7 @@
    7.49  Delsimps [FilterConc]; 
    7.50  
    7.51  
    7.52 -Goal " !!as. [| Finite as; is_asig(asig_of A); is_asig(asig_of B);compatible A B|] ==>  \
    7.53 +Goal " [| Finite as; is_asig(asig_of A); is_asig(asig_of B);compatible A B|] ==>  \
    7.54  \! x. Forall (%x. x:act A) x & Forall (%x. x:act A & x~:act B) as &\
    7.55  \    Filter (%a. a:ext A)`x = Filter (%a. a:act A)`(as @@ z) \
    7.56  \    --> (? x1 x2.  (mksch A B`(as @@ z)`x`y) = (x1 @@ (mksch A B`z`x2`y)) & \
    7.57 @@ -379,7 +379,7 @@
    7.58  (*
    7.59  
    7.60  
    7.61 -Goal "!! y.Finite y ==> ! z tr. Forall (%a.a:ext (A||B)) tr & \
    7.62 +Goal "Finite y ==> ! z tr. Forall (%a.a:ext (A||B)) tr & \
    7.63  \                             y = z @@ mksch A B`tr`a`b\
    7.64  \                             --> Finite tr";
    7.65  by (etac Seq_Finite_ind  1);
     8.1 --- a/src/HOLCF/IOA/meta_theory/Compositionality.ML	Thu Jan 28 18:28:06 1999 +0100
     8.2 +++ b/src/HOLCF/IOA/meta_theory/Compositionality.ML	Fri Jan 29 16:23:56 1999 +0100
     8.3 @@ -8,7 +8,7 @@
     8.4  
     8.5  
     8.6  
     8.7 -Goal "!! A. [|eA --> A ; eB & ~eA --> ~A|] ==> (eA | eB) --> A=eA";
     8.8 +Goal "[|eA --> A ; eB & ~eA --> ~A|] ==> (eA | eB) --> A=eA";
     8.9  by Auto_tac;
    8.10  qed"compatibility_consequence3";
    8.11  
    8.12 @@ -27,12 +27,11 @@
    8.13  
    8.14  (* the next two theorems are only necessary, as there is no theorem ext (A||B) = ext (B||A) *)
    8.15  
    8.16 -Goal "!! A. [|eA --> A ; eB & ~eA --> ~A|] ==> (eB | eA) --> A=eA";
    8.17 +Goal "[|eA --> A ; eB & ~eA --> ~A|] ==> (eB | eA) --> A=eA";
    8.18  by Auto_tac;
    8.19  qed"compatibility_consequence4";
    8.20  
    8.21 -Goal 
    8.22 -"!! A B. [| compatible A B; Forall (%a. a: ext B | a: ext A) tr |] ==> \
    8.23 +Goal "[| compatible A B; Forall (%a. a: ext B | a: ext A) tr |] ==> \
    8.24  \           Filter (%a. a: act A)`tr= Filter (%a. a: ext A)`tr";
    8.25  by (rtac ForallPFilterQR 1);
    8.26  by (assume_tac 2);
    8.27 @@ -48,8 +47,7 @@
    8.28  
    8.29  
    8.30  
    8.31 -Goal "!! A1 A2 B1 B2. \
    8.32 -\         [| is_trans_of A1; is_trans_of A2; is_trans_of B1; is_trans_of B2;\
    8.33 +Goal "[| is_trans_of A1; is_trans_of A2; is_trans_of B1; is_trans_of B2;\
    8.34  \            is_asig_of A1; is_asig_of A2; \
    8.35  \            is_asig_of B1; is_asig_of B2; \
    8.36  \            compatible A1 B1; compatible A2 B2; \
     9.1 --- a/src/HOLCF/IOA/meta_theory/Deadlock.ML	Thu Jan 28 18:28:06 1999 +0100
     9.2 +++ b/src/HOLCF/IOA/meta_theory/Deadlock.ML	Fri Jan 29 16:23:56 1999 +0100
     9.3 @@ -10,14 +10,14 @@
     9.4                 input actions may always be added to a schedule
     9.5  **********************************************************************************)
     9.6  
     9.7 -Goal "!! sch. [| Filter (%x. x:act A)`sch : schedules A; a:inp A; input_enabled A; Finite sch|] \
     9.8 +Goal "[| Filter (%x. x:act A)`sch : schedules A; a:inp A; input_enabled A; Finite sch|] \
     9.9  \         ==> Filter (%x. x:act A)`sch @@ a>>nil : schedules A";
    9.10  by (asm_full_simp_tac (simpset() addsimps [schedules_def,has_schedule_def]) 1);
    9.11  by (safe_tac set_cs);
    9.12  by (forward_tac  [inp_is_act] 1);
    9.13  by (asm_full_simp_tac (simpset() addsimps [executions_def]) 1);
    9.14  by (pair_tac "ex" 1);
    9.15 -ren "sch s ex" 1;
    9.16 +ren "s ex" 1;
    9.17  by (subgoal_tac "Finite ex" 1);
    9.18  by (asm_full_simp_tac (simpset() addsimps [filter_act_def]) 2);
    9.19  by (rtac (Map2Finite RS iffD1) 2);
    9.20 @@ -51,7 +51,7 @@
    9.21                      and distributivity of is_exec_frag over @@
    9.22  **********************************************************************************)
    9.23  Delsplits [split_if];
    9.24 -Goal "!! sch. [| a : local A; Finite sch; sch : schedules (A||B); \
    9.25 +Goal "[| a : local A; Finite sch; sch : schedules (A||B); \
    9.26  \            Filter (%x. x:act A)`(sch @@ a>>nil) : schedules A; compatible A B; input_enabled B |] \
    9.27  \          ==> (sch @@ a>>nil) : schedules (A||B)";
    9.28  
    10.1 --- a/src/HOLCF/IOA/meta_theory/LiveIOA.ML	Thu Jan 28 18:28:06 1999 +0100
    10.2 +++ b/src/HOLCF/IOA/meta_theory/LiveIOA.ML	Fri Jan 29 16:23:56 1999 +0100
    10.3 @@ -10,7 +10,7 @@
    10.4  Delsimps [split_paired_Ex];
    10.5  
    10.6  Goalw [live_implements_def] 
    10.7 -"!! A. [| live_implements (A,LA) (B,LB); live_implements (B,LB) (C,LC) |] \
    10.8 +"[| live_implements (A,LA) (B,LB); live_implements (B,LB) (C,LC) |] \
    10.9  \     ==> live_implements (A,LA) (C,LC)"; 
   10.10  by Auto_tac;
   10.11  qed"live_implements_trans";
   10.12 @@ -24,7 +24,7 @@
   10.13  (* ---------------------------------------------------------------- *)
   10.14  
   10.15  
   10.16 -Goal "!! f. [| inp(C)=inp(A); out(C)=out(A); \
   10.17 +Goal "[| inp(C)=inp(A); out(C)=out(A); \
   10.18  \                  is_live_ref_map f (C,M) (A,L) |] \
   10.19  \               ==> live_implements (C,M) (A,L)";
   10.20  
    11.1 --- a/src/HOLCF/IOA/meta_theory/RefCorrectness.ML	Thu Jan 28 18:28:06 1999 +0100
    11.2 +++ b/src/HOLCF/IOA/meta_theory/RefCorrectness.ML	Fri Jan 29 16:23:56 1999 +0100
    11.3 @@ -62,7 +62,7 @@
    11.4  section"properties of move";
    11.5  
    11.6  Goalw [is_ref_map_def]
    11.7 -   "!!f. [|is_ref_map f C A; reachable C s; (s,a,t):trans_of C|] ==>\
    11.8 +   "[|is_ref_map f C A; reachable C s; (s,a,t):trans_of C|] ==>\
    11.9  \     move A (@x. move A x (f s) a (f t)) (f s) a (f t)";
   11.10  
   11.11  by (subgoal_tac "? ex. move A ex (f s) a (f t)" 1);
   11.12 @@ -73,7 +73,7 @@
   11.13  qed"move_is_move";
   11.14  
   11.15  Goal
   11.16 -   "!!f. [|is_ref_map f C A; reachable C s; (s,a,t):trans_of C|] ==>\
   11.17 +   "[|is_ref_map f C A; reachable C s; (s,a,t):trans_of C|] ==>\
   11.18  \    is_exec_frag A (f s,@x. move A x (f s) a (f t))";
   11.19  by (cut_inst_tac [] move_is_move 1);
   11.20  by (REPEAT (assume_tac 1));
   11.21 @@ -81,7 +81,7 @@
   11.22  qed"move_subprop1";
   11.23  
   11.24  Goal
   11.25 -   "!!f. [|is_ref_map f C A; reachable C s; (s,a,t):trans_of C|] ==>\
   11.26 +   "[|is_ref_map f C A; reachable C s; (s,a,t):trans_of C|] ==>\
   11.27  \    Finite ((@x. move A x (f s) a (f t)))";
   11.28  by (cut_inst_tac [] move_is_move 1);
   11.29  by (REPEAT (assume_tac 1));
   11.30 @@ -89,7 +89,7 @@
   11.31  qed"move_subprop2";
   11.32  
   11.33  Goal
   11.34 -   "!!f. [|is_ref_map f C A; reachable C s; (s,a,t):trans_of C|] ==>\
   11.35 +   "[|is_ref_map f C A; reachable C s; (s,a,t):trans_of C|] ==>\
   11.36  \    laststate (f s,@x. move A x (f s) a (f t)) = (f t)";
   11.37  by (cut_inst_tac [] move_is_move 1);
   11.38  by (REPEAT (assume_tac 1));
   11.39 @@ -97,7 +97,7 @@
   11.40  qed"move_subprop3";
   11.41  
   11.42  Goal
   11.43 -   "!!f. [|is_ref_map f C A; reachable C s; (s,a,t):trans_of C|] ==>\
   11.44 +   "[|is_ref_map f C A; reachable C s; (s,a,t):trans_of C|] ==>\
   11.45  \     mk_trace A`((@x. move A x (f s) a (f t))) = \
   11.46  \       (if a:ext A then a>>nil else nil)";
   11.47  
   11.48 @@ -131,7 +131,7 @@
   11.49     ------------------------------------------------------- *)
   11.50  Delsplits[split_if];
   11.51  Goalw [corresp_ex_def]
   11.52 -  "!!f.[|is_ref_map f C A; ext C = ext A|] ==>  \     
   11.53 +  "[|is_ref_map f C A; ext C = ext A|] ==>  \     
   11.54  \        !s. reachable C s & is_exec_frag C (s,xs) --> \
   11.55  \            mk_trace C`xs = mk_trace A`(snd (corresp_ex A f (s,xs)))";
   11.56  
   11.57 @@ -180,7 +180,7 @@
   11.58  
   11.59  
   11.60  Goalw [corresp_ex_def]
   11.61 - "!!f.[| is_ref_map f C A |] ==>\
   11.62 + "[| is_ref_map f C A |] ==>\
   11.63  \ !s. reachable C s & is_exec_frag C (s,xs) \
   11.64  \ --> is_exec_frag A (corresp_ex A f (s,xs))"; 
   11.65  
   11.66 @@ -221,7 +221,7 @@
   11.67  
   11.68  
   11.69  Goalw [traces_def]
   11.70 -  "!!f. [| ext C = ext A; is_ref_map f C A |] \
   11.71 +  "[| ext C = ext A; is_ref_map f C A |] \
   11.72  \          ==> traces C <= traces A"; 
   11.73  
   11.74    by (simp_tac(simpset() addsimps [has_trace_def2])1);
   11.75 @@ -260,15 +260,13 @@
   11.76  qed"fininf";
   11.77  
   11.78  
   11.79 -Goal 
   11.80 -"is_wfair A W (s,ex) = \
   11.81 +Goal "is_wfair A W (s,ex) = \
   11.82  \ (fin_often (%x. ~Enabled A W (snd x)) ex --> inf_often (%x. fst x :W) ex)";
   11.83  by (asm_full_simp_tac (simpset() addsimps [is_wfair_def,fin_often_def])1);
   11.84  by Auto_tac;
   11.85  qed"WF_alt";
   11.86  
   11.87 -Goal  
   11.88 -"!! ex. [|is_wfair A W (s,ex); inf_often (%x. Enabled A W (snd x)) ex; \
   11.89 +Goal "[|is_wfair A W (s,ex); inf_often (%x. Enabled A W (snd x)) ex; \
   11.90  \         en_persistent A W|] \
   11.91  \   ==> inf_often (%x. fst x :W) ex";
   11.92  by (dtac persistent 1);
    12.1 --- a/src/HOLCF/IOA/meta_theory/RefMappings.ML	Thu Jan 28 18:28:06 1999 +0100
    12.2 +++ b/src/HOLCF/IOA/meta_theory/RefMappings.ML	Fri Jan 29 16:23:56 1999 +0100
    12.3 @@ -15,21 +15,21 @@
    12.4  section "transitions and moves";
    12.5  
    12.6  
    12.7 -Goal"!!f. s -a--A-> t ==> ? ex. move A ex s a t";
    12.8 +Goal "s -a--A-> t ==> ? ex. move A ex s a t";
    12.9  
   12.10  by (res_inst_tac [("x","(a,t)>>nil")] exI 1);
   12.11  by (asm_full_simp_tac (simpset() addsimps [move_def]) 1);
   12.12  qed"transition_is_ex";
   12.13   
   12.14  
   12.15 -Goal"!!f. (~a:ext A) & s=t ==> ? ex. move A ex s a t";
   12.16 +Goal "(~a:ext A) & s=t ==> ? ex. move A ex s a t";
   12.17  
   12.18  by (res_inst_tac [("x","nil")] exI 1);
   12.19  by (asm_full_simp_tac (simpset() addsimps [move_def]) 1);
   12.20  qed"nothing_is_ex";
   12.21  
   12.22  
   12.23 -Goal"!!f. (s -a--A-> s') & (s' -a'--A-> s'') & (~a':ext A) \
   12.24 +Goal "(s -a--A-> s') & (s' -a'--A-> s'') & (~a':ext A) \
   12.25  \        ==> ? ex. move A ex s a s''";
   12.26  
   12.27  by (res_inst_tac [("x","(a,s')>>(a',s'')>>nil")] exI 1);
   12.28 @@ -37,8 +37,7 @@
   12.29  qed"ei_transitions_are_ex";
   12.30  
   12.31  
   12.32 -Goal
   12.33 -"!!f. (s1 -a1--A-> s2) & (s2 -a2--A-> s3) & (s3 -a3--A-> s4) &\
   12.34 +Goal "(s1 -a1--A-> s2) & (s2 -a2--A-> s3) & (s3 -a3--A-> s4) &\
   12.35  \     (~a2:ext A) & (~a3:ext A) ==> \
   12.36  \     ? ex. move A ex s1 a1 s4";
   12.37    
   12.38 @@ -53,7 +52,7 @@
   12.39  
   12.40  
   12.41  Goalw [is_weak_ref_map_def,is_ref_map_def]
   12.42 -  "!!f. [| ext C = ext A; \
   12.43 +  "[| ext C = ext A; \
   12.44  \    is_weak_ref_map f C A |] ==> is_ref_map f C A";
   12.45  by (safe_tac set_cs);
   12.46  by (case_tac "a:ext A" 1);
   12.47 @@ -69,7 +68,7 @@
   12.48  val lemma = result();
   12.49  
   12.50  Delsplits [split_if];
   12.51 -Goal "!!f.[| is_weak_ref_map f C A |]\
   12.52 +Goal "[| is_weak_ref_map f C A |]\
   12.53  \                      ==> (is_weak_ref_map f (rename C g) (rename A g))";
   12.54  by (asm_full_simp_tac (simpset() addsimps [is_weak_ref_map_def]) 1);
   12.55  by (rtac conjI 1);
    13.1 --- a/src/HOLCF/IOA/meta_theory/Seq.ML	Thu Jan 28 18:28:06 1999 +0100
    13.2 +++ b/src/HOLCF/IOA/meta_theory/Seq.ML	Fri Jan 29 16:23:56 1999 +0100
    13.3 @@ -47,7 +47,7 @@
    13.4  qed"smap_UU";
    13.5  
    13.6  Goal 
    13.7 -"!!x.[|x~=UU|] ==> smap`f`(x##xs)= (f`x)##smap`f`xs"; 
    13.8 +"[|x~=UU|] ==> smap`f`(x##xs)= (f`x)##smap`f`xs"; 
    13.9  by (rtac trans 1);
   13.10  by (stac smap_unfold 1);
   13.11  by (Asm_full_simp_tac 1);
   13.12 @@ -74,7 +74,7 @@
   13.13  qed"sfilter_UU";
   13.14  
   13.15  Goal 
   13.16 -"!!x. x~=UU ==> sfilter`P`(x##xs)=   \
   13.17 +"x~=UU ==> sfilter`P`(x##xs)=   \
   13.18  \             (If P`x then x##(sfilter`P`xs) else sfilter`P`xs fi)";
   13.19  by (rtac trans 1);
   13.20  by (stac sfilter_unfold 1);
   13.21 @@ -102,7 +102,7 @@
   13.22  qed"sforall2_UU";
   13.23  
   13.24  Goal 
   13.25 -"!!x. x~=UU ==> sforall2`P`(x##xs)= ((P`x) andalso sforall2`P`xs)";
   13.26 +"x~=UU ==> sforall2`P`(x##xs)= ((P`x) andalso sforall2`P`xs)";
   13.27  by (rtac trans 1);
   13.28  by (stac sforall2_unfold 1);
   13.29  by (Asm_full_simp_tac 1);
   13.30 @@ -131,7 +131,7 @@
   13.31  qed"stakewhile_UU";
   13.32  
   13.33  Goal 
   13.34 -"!!x. x~=UU ==> stakewhile`P`(x##xs) =   \
   13.35 +"x~=UU ==> stakewhile`P`(x##xs) =   \
   13.36  \             (If P`x then x##(stakewhile`P`xs) else nil fi)";
   13.37  by (rtac trans 1);
   13.38  by (stac stakewhile_unfold 1);
   13.39 @@ -160,7 +160,7 @@
   13.40  qed"sdropwhile_UU";
   13.41  
   13.42  Goal 
   13.43 -"!!x. x~=UU ==> sdropwhile`P`(x##xs) =   \
   13.44 +"x~=UU ==> sdropwhile`P`(x##xs) =   \
   13.45  \             (If P`x then sdropwhile`P`xs else x##xs fi)";
   13.46  by (rtac trans 1);
   13.47  by (stac sdropwhile_unfold 1);
   13.48 @@ -191,7 +191,7 @@
   13.49  qed"slast_UU";
   13.50  
   13.51  Goal 
   13.52 -"!!x. x~=UU ==> slast`(x##xs)= (If is_nil`xs then x else slast`xs fi)";
   13.53 +"x~=UU ==> slast`(x##xs)= (If is_nil`xs then x else slast`xs fi)";
   13.54  by (rtac trans 1);
   13.55  by (stac slast_unfold 1);
   13.56  by (Asm_full_simp_tac 1);
   13.57 @@ -281,20 +281,20 @@
   13.58  by (Simp_tac 1);
   13.59  qed"szip_UU1";
   13.60  
   13.61 -Goal "!!x. x~=nil ==> szip`x`UU=UU"; 
   13.62 +Goal "x~=nil ==> szip`x`UU=UU"; 
   13.63  by (stac szip_unfold 1);
   13.64  by (Asm_full_simp_tac 1);
   13.65  by (res_inst_tac [("x","x")] seq.casedist 1);
   13.66  by (REPEAT (Asm_full_simp_tac 1));
   13.67  qed"szip_UU2";
   13.68  
   13.69 -Goal "!!x. x~=UU ==> szip`(x##xs)`nil=UU";
   13.70 +Goal "x~=UU ==> szip`(x##xs)`nil=UU";
   13.71  by (rtac trans 1);
   13.72  by (stac szip_unfold 1);
   13.73  by (REPEAT (Asm_full_simp_tac 1));
   13.74  qed"szip_cons_nil";
   13.75  
   13.76 -Goal "!!x.[| x~=UU; y~=UU|] ==> szip`(x##xs)`(y##ys) = <x,y>##szip`xs`ys";
   13.77 +Goal "[| x~=UU; y~=UU|] ==> szip`(x##xs)`(y##ys) = <x,y>##szip`xs`ys";
   13.78  by (rtac trans 1);
   13.79  by (stac szip_unfold 1);
   13.80  by (REPEAT (Asm_full_simp_tac 1));
   13.81 @@ -317,13 +317,13 @@
   13.82  section "scons, nil";
   13.83  
   13.84  Goal 
   13.85 - "!!x. [|x~=UU;y~=UU|]==> (x##xs=y##ys) = (x=y & xs=ys)";
   13.86 + "[|x~=UU;y~=UU|]==> (x##xs=y##ys) = (x=y & xs=ys)";
   13.87  by (rtac iffI 1);
   13.88  by (etac (hd seq.injects) 1);
   13.89  by Auto_tac;
   13.90  qed"scons_inject_eq";
   13.91  
   13.92 -Goal "!!x. nil<<x ==> nil=x";
   13.93 +Goal "nil<<x ==> nil=x";
   13.94  by (res_inst_tac [("x","x")] seq.casedist 1);
   13.95  by (hyp_subst_tac 1);
   13.96  by (etac antisym_less 1);
   13.97 @@ -416,7 +416,7 @@
   13.98  by (fast_tac (HOL_cs addSDs seq.injects) 1);
   13.99  qed"Finite_cons_a";
  13.100  
  13.101 -Goal "!!x. a~=UU ==>(Finite (a##x)) = (Finite x)";
  13.102 +Goal "a~=UU ==>(Finite (a##x)) = (Finite x)";
  13.103  by (rtac iffI 1);
  13.104  by (rtac (Finite_cons_a RS mp RS mp RS mp) 1);
  13.105  by (REPEAT (assume_tac 1));
  13.106 @@ -448,8 +448,7 @@
  13.107          ]);
  13.108  
  13.109  
  13.110 -Goal 
  13.111 -"!!P.[|P(UU);P(nil);\
  13.112 +Goal "!!P.[|P(UU);P(nil);\
  13.113  \  !! x s1.[|x~=UU;P(s1)|] ==> P(x##s1)\
  13.114  \  |] ==> seq_finite(s) --> P(s)";
  13.115  by (rtac seq_finite_ind_lemma 1);
    14.1 --- a/src/HOLCF/IOA/meta_theory/Sequence.ML	Thu Jan 28 18:28:06 1999 +0100
    14.2 +++ b/src/HOLCF/IOA/meta_theory/Sequence.ML	Fri Jan 29 16:23:56 1999 +0100
    14.3 @@ -167,7 +167,7 @@
    14.4  by (Simp_tac 1);
    14.5  qed"Zip_UU1";
    14.6  
    14.7 -Goal "!! x. x~=nil ==> Zip`x`UU =UU";
    14.8 +Goal "x~=nil ==> Zip`x`UU =UU";
    14.9  by (stac Zip_unfold 1);
   14.10  by (Simp_tac 1);
   14.11  by (res_inst_tac [("x","x")] seq.casedist 1);
   14.12 @@ -384,11 +384,11 @@
   14.13  qed"Finite_Cons";
   14.14  
   14.15  Addsimps [Finite_Cons];
   14.16 -Goal "!! x. Finite (x::'a Seq) ==> Finite y --> Finite (x@@y)";
   14.17 +Goal "Finite (x::'a Seq) ==> Finite y --> Finite (x@@y)";
   14.18  by (Seq_Finite_induct_tac 1);
   14.19  qed"FiniteConc_1";
   14.20  
   14.21 -Goal "!! z. Finite (z::'a Seq) ==> !x y. z= x@@y --> (Finite x & Finite y)";
   14.22 +Goal "Finite (z::'a Seq) ==> !x y. z= x@@y --> (Finite x & Finite y)";
   14.23  by (Seq_Finite_induct_tac 1);
   14.24  (* nil*)
   14.25  by (strip_tac 1);
   14.26 @@ -415,11 +415,11 @@
   14.27  Addsimps [FiniteConc];
   14.28  
   14.29  
   14.30 -Goal "!! s. Finite s ==> Finite (Map f`s)";
   14.31 +Goal "Finite s ==> Finite (Map f`s)";
   14.32  by (Seq_Finite_induct_tac 1);
   14.33  qed"FiniteMap1";
   14.34  
   14.35 -Goal "!! s. Finite s ==> ! t. (s = Map f`t) --> Finite t";
   14.36 +Goal "Finite s ==> ! t. (s = Map f`t) --> Finite t";
   14.37  by (Seq_Finite_induct_tac 1);
   14.38  by (strip_tac 1);
   14.39  by (Seq_case_simp_tac "t" 1);
   14.40 @@ -438,7 +438,7 @@
   14.41  qed"Map2Finite";
   14.42  
   14.43  
   14.44 -Goal "!! s. Finite s ==> Finite (Filter P`s)";
   14.45 +Goal "Finite s ==> Finite (Filter P`s)";
   14.46  by (Seq_Finite_induct_tac 1);
   14.47  qed"FiniteFilter";
   14.48  
   14.49 @@ -519,11 +519,11 @@
   14.50  
   14.51  section "Last";
   14.52  
   14.53 -Goal "!! s. Finite s ==> s~=nil --> Last`s~=UU";
   14.54 +Goal "Finite s ==> s~=nil --> Last`s~=UU";
   14.55  by (Seq_Finite_induct_tac  1);
   14.56  qed"Finite_Last1";
   14.57  
   14.58 -Goal "!! s. Finite s ==> Last`s=UU --> s=nil";
   14.59 +Goal "Finite s ==> Last`s=UU --> s=nil";
   14.60  by (Seq_Finite_induct_tac  1);
   14.61  by (fast_tac HOL_cs 1);
   14.62  qed"Finite_Last2";
   14.63 @@ -587,7 +587,7 @@
   14.64  by (Seq_induct_tac "x" [Forall_def,sforall_def] 1);
   14.65  qed"Forall_Conc_impl";
   14.66  
   14.67 -Goal "!! x. Finite x ==> Forall P (x @@ y) = (Forall P x & Forall P y)";
   14.68 +Goal "Finite x ==> Forall P (x @@ y) = (Forall P x & Forall P y)";
   14.69  by (Seq_Finite_induct_tac  1);
   14.70  qed"Forall_Conc";
   14.71  
   14.72 @@ -619,7 +619,7 @@
   14.73  bind_thm ("Forall_prefixclosed",Forall_prefix RS spec RS mp RS mp);
   14.74  
   14.75  
   14.76 -Goal "!! h. [| Finite h; Forall P s; s= h @@ t |] ==> Forall P t";
   14.77 +Goal "[| Finite h; Forall P s; s= h @@ t |] ==> Forall P t";
   14.78  by Auto_tac;
   14.79  qed"Forall_postfixclosed";
   14.80  
   14.81 @@ -658,7 +658,7 @@
   14.82  
   14.83  
   14.84  (* holds also in other direction *)
   14.85 -Goal   "!! P. ~Finite ys & Forall (%x. ~P x) ys \
   14.86 +Goal   "~Finite ys & Forall (%x. ~P x) ys \
   14.87  \                  --> Filter P`ys = UU ";
   14.88  by (Seq_induct_tac "ys" [Forall_def,sforall_def] 1);
   14.89  qed"ForallnPFilterPUU1";
   14.90 @@ -685,7 +685,7 @@
   14.91  
   14.92  (* inverse of ForallnPFilterPUU. proved by 2 lemmas because of adm problems *)
   14.93  
   14.94 -Goal "!! ys. Finite ys ==> Filter P`ys ~= UU";
   14.95 +Goal "Finite ys ==> Filter P`ys ~= UU";
   14.96  by (Seq_Finite_induct_tac 1);
   14.97  qed"FilterUU_nFinite_lemma1";
   14.98  
   14.99 @@ -693,7 +693,7 @@
  14.100  by (Seq_induct_tac "ys" [Forall_def,sforall_def] 1);
  14.101  qed"FilterUU_nFinite_lemma2";
  14.102  
  14.103 -Goal   "!! P. Filter P`ys = UU ==> \
  14.104 +Goal   "Filter P`ys = UU ==> \
  14.105  \                (Forall (%x. ~P x) ys  & ~Finite ys)";
  14.106  by (rtac conjI 1);
  14.107  by (cut_inst_tac [] (FilterUU_nFinite_lemma2 RS mp COMP rev_contrapos) 1);
  14.108 @@ -775,7 +775,7 @@
  14.109  
  14.110  bind_thm("TakewhileConc",TakewhileConc1 RS mp);
  14.111  
  14.112 -Goal "!! s. Finite s ==> Forall P s --> Dropwhile P`(s @@ t) = Dropwhile P`t";
  14.113 +Goal "Finite s ==> Forall P s --> Dropwhile P`(s @@ t) = Dropwhile P`t";
  14.114  by (Seq_Finite_induct_tac 1);
  14.115  qed"DropwhileConc1";
  14.116  
  14.117 @@ -804,7 +804,7 @@
  14.118  by (Asm_full_simp_tac 1); 
  14.119  qed"divide_Seq_lemma";
  14.120  
  14.121 -Goal "!! x. (x>>xs) << Filter P`y  \
  14.122 +Goal "(x>>xs) << Filter P`y  \
  14.123  \   ==> y = ((Takewhile (%a. ~ P a)`y) @@ (x >> TL`(Dropwhile (%a.~P a)`y))) \
  14.124  \      & Finite (Takewhile (%a. ~ P a)`y)  & P x";
  14.125  by (rtac (divide_Seq_lemma RS mp) 1);
  14.126 @@ -820,7 +820,7 @@
  14.127  qed"nForall_HDFilter";
  14.128  
  14.129  
  14.130 -Goal "!!y. ~Forall P y  \
  14.131 +Goal "~Forall P y  \
  14.132  \  ==> ? x. y= (Takewhile P`y @@ (x >> TL`(Dropwhile P`y))) & \
  14.133  \      Finite (Takewhile P`y) & (~ P x)";
  14.134  by (dtac (nForall_HDFilter RS mp) 1);
  14.135 @@ -831,7 +831,7 @@
  14.136  qed"divide_Seq2";
  14.137  
  14.138  
  14.139 -Goal  "!! y. ~Forall P y \
  14.140 +Goal  "~Forall P y \
  14.141  \  ==> ? x bs rs. y= (bs @@ (x>>rs)) & Finite bs & Forall P bs & (~ P x)";
  14.142  by (cut_inst_tac [] divide_Seq2 1);
  14.143  (*Auto_tac no longer proves it*)
  14.144 @@ -864,7 +864,7 @@
  14.145  qed"take_reduction1";
  14.146  
  14.147  
  14.148 -Goal "!! n.[| x=y; s=t;!! k. k<n ==> seq_take k`y1 = seq_take k`y2|] \
  14.149 +Goal "!! n.[| x=y; s=t; !! k. k<n ==> seq_take k`y1 = seq_take k`y2|] \
  14.150  \ ==> seq_take n`(x @@ (s>>y1)) =  seq_take n`(y @@ (t>>y2))";
  14.151  
  14.152  by (auto_tac (claset() addSIs [take_reduction1 RS spec RS mp],simpset()));
  14.153 @@ -1117,13 +1117,13 @@
  14.154  by (Seq_induct_tac "s" [Forall_def,sforall_def] 1);
  14.155  qed"Filter_lemma1";
  14.156  
  14.157 -Goal "!! s. Finite s ==>  \
  14.158 +Goal "Finite s ==>  \
  14.159  \         (Forall (%x. (~P x) | (~ Q x)) s  \
  14.160  \         --> Filter P`(Filter Q`s) = nil)";
  14.161  by (Seq_Finite_induct_tac 1);
  14.162  qed"Filter_lemma2";
  14.163  
  14.164 -Goal "!! s. Finite s ==>  \
  14.165 +Goal "Finite s ==>  \
  14.166  \         Forall (%x. (~P x) | (~ Q x)) s  \
  14.167  \         --> Filter (%x. P x & Q x)`s = nil";
  14.168  by (Seq_Finite_induct_tac 1);
    15.1 --- a/src/HOLCF/IOA/meta_theory/ShortExecutions.ML	Thu Jan 28 18:28:06 1999 +0100
    15.2 +++ b/src/HOLCF/IOA/meta_theory/ShortExecutions.ML	Fri Jan 29 16:23:56 1999 +0100
    15.3 @@ -61,7 +61,7 @@
    15.4  (* ---------------------------------------------------------------- *)
    15.5  
    15.6  Goalw [Cut_def]
    15.7 -"!! s. [| Forall (%a.~ P a) s; Finite s|] \
    15.8 +"[| Forall (%a.~ P a) s; Finite s|] \
    15.9  \           ==> Cut P s =nil";
   15.10  by (subgoal_tac "Filter P`s = nil" 1);
   15.11  by (asm_simp_tac (simpset() addsimps [oraclebuild_nil]) 1);
   15.12 @@ -70,7 +70,7 @@
   15.13  qed"Cut_nil";
   15.14  
   15.15  Goalw [Cut_def]
   15.16 -"!! s. [| Forall (%a.~ P a) s; ~Finite s|] \
   15.17 +"[| Forall (%a.~ P a) s; ~Finite s|] \
   15.18  \           ==> Cut P s =UU";
   15.19  by (subgoal_tac "Filter P`s= UU" 1);
   15.20  by (asm_simp_tac (simpset() addsimps [oraclebuild_UU]) 1);
   15.21 @@ -79,7 +79,7 @@
   15.22  qed"Cut_UU";
   15.23  
   15.24  Goalw [Cut_def]
   15.25 -"!! s. [| P t;  Forall (%x.~ P x) ss; Finite ss|] \
   15.26 +"[| P t;  Forall (%x.~ P x) ss; Finite ss|] \
   15.27  \           ==> Cut P (ss @@ (t>> rs)) \
   15.28  \                = ss @@ (t >> Cut P rs)";
   15.29  
   15.30 @@ -200,7 +200,7 @@
   15.31  
   15.32  
   15.33  Goalw [schedules_def,has_schedule_def]
   15.34 - "!! sch. [|sch : schedules A ; tr = Filter (%a. a:ext A)`sch|] \
   15.35 + "[|sch : schedules A ; tr = Filter (%a. a:ext A)`sch|] \
   15.36  \   ==> ? sch. sch : schedules A & \
   15.37  \              tr = Filter (%a. a:ext A)`sch &\
   15.38  \              LastActExtsch A sch";
   15.39 @@ -239,7 +239,7 @@
   15.40  (* ---------------------------------------------------------------- *)
   15.41  
   15.42  Goalw [LastActExtsch_def]
   15.43 -  "!! A. [| LastActExtsch A sch; Filter (%x. x:ext A)`sch = nil |] \
   15.44 +  "[| LastActExtsch A sch; Filter (%x. x:ext A)`sch = nil |] \
   15.45  \   ==> sch=nil";
   15.46  by (dtac FilternPnilForallP 1);
   15.47  by (etac conjE 1);
   15.48 @@ -249,7 +249,7 @@
   15.49  qed"LastActExtimplnil";
   15.50  
   15.51  Goalw [LastActExtsch_def]
   15.52 -  "!! A. [| LastActExtsch A sch; Filter (%x. x:ext A)`sch = UU |] \
   15.53 +  "[| LastActExtsch A sch; Filter (%x. x:ext A)`sch = UU |] \
   15.54  \   ==> sch=UU";
   15.55  by (dtac FilternPUUForallP 1);
   15.56  by (etac conjE 1);
    16.1 --- a/src/HOLCF/IOA/meta_theory/SimCorrectness.ML	Thu Jan 28 18:28:06 1999 +0100
    16.2 +++ b/src/HOLCF/IOA/meta_theory/SimCorrectness.ML	Fri Jan 29 16:23:56 1999 +0100
    16.3 @@ -69,7 +69,7 @@
    16.4  Delsimps [Let_def];
    16.5  
    16.6  Goalw [is_simulation_def]
    16.7 -   "!!f. [|is_simulation R C A; reachable C s; s -a--C-> t; (s,s'):R|] ==>\
    16.8 +   "[|is_simulation R C A; reachable C s; s -a--C-> t; (s,s'):R|] ==>\
    16.9  \     let T' = @t'. ? ex1. (t,t'):R & move A ex1 s' a t' in \
   16.10  \     (t,T'): R & move A (@ex2. move A ex2 s' a T') s' a T'";
   16.11  
   16.12 @@ -99,7 +99,7 @@
   16.13  Addsimps [Let_def];
   16.14  
   16.15  Goal
   16.16 -   "!!f. [|is_simulation R C A; reachable C s; s-a--C-> t; (s,s'):R|] ==>\
   16.17 +   "[|is_simulation R C A; reachable C s; s-a--C-> t; (s,s'):R|] ==>\
   16.18  \   let T' = @t'. ? ex1. (t,t'):R & move A ex1 s' a t' in \
   16.19  \    is_exec_frag A (s',@x. move A x s' a T')";
   16.20  by (cut_inst_tac [] move_is_move_sim 1);
   16.21 @@ -108,7 +108,7 @@
   16.22  qed"move_subprop1_sim";
   16.23  
   16.24  Goal
   16.25 -   "!!f. [|is_simulation R C A; reachable C s; s-a--C-> t; (s,s'):R|] ==>\
   16.26 +   "[|is_simulation R C A; reachable C s; s-a--C-> t; (s,s'):R|] ==>\
   16.27  \   let T' = @t'. ? ex1. (t,t'):R & move A ex1 s' a t' in \
   16.28  \   Finite (@x. move A x s' a T')";
   16.29  by (cut_inst_tac [] move_is_move_sim 1);
   16.30 @@ -117,7 +117,7 @@
   16.31  qed"move_subprop2_sim";
   16.32  
   16.33  Goal
   16.34 -   "!!f. [|is_simulation R C A; reachable C s; s-a--C-> t; (s,s'):R|] ==>\
   16.35 +   "[|is_simulation R C A; reachable C s; s-a--C-> t; (s,s'):R|] ==>\
   16.36  \   let T' = @t'. ? ex1. (t,t'):R & move A ex1 s' a t' in \
   16.37  \    laststate (s',@x. move A x s' a T') = T'";
   16.38  by (cut_inst_tac [] move_is_move_sim 1);
   16.39 @@ -126,7 +126,7 @@
   16.40  qed"move_subprop3_sim";
   16.41  
   16.42  Goal
   16.43 -   "!!f. [|is_simulation R C A; reachable C s; s-a--C-> t; (s,s'):R|] ==>\
   16.44 +   "[|is_simulation R C A; reachable C s; s-a--C-> t; (s,s'):R|] ==>\
   16.45  \   let T' = @t'. ? ex1. (t,t'):R & move A ex1 s' a t' in \
   16.46  \     mk_trace A`((@x. move A x s' a T')) = \
   16.47  \       (if a:ext A then a>>nil else nil)";
   16.48 @@ -136,7 +136,7 @@
   16.49  qed"move_subprop4_sim";
   16.50  
   16.51  Goal
   16.52 -   "!!f. [|is_simulation R C A; reachable C s; s-a--C-> t; (s,s'):R|] ==>\
   16.53 +   "[|is_simulation R C A; reachable C s; s-a--C-> t; (s,s'):R|] ==>\
   16.54  \   let T' = @t'. ? ex1. (t,t'):R & move A ex1 s' a t' in \
   16.55  \     (t,T'):R";
   16.56  by (cut_inst_tac [] move_is_move_sim 1);
   16.57 @@ -158,7 +158,7 @@
   16.58  
   16.59  Delsplits[split_if];
   16.60  Goal 
   16.61 -  "!!f.[|is_simulation R C A; ext C = ext A|] ==>  \     
   16.62 +  "[|is_simulation R C A; ext C = ext A|] ==>  \     
   16.63  \        !s s'. reachable C s & is_exec_frag C (s,ex) & (s,s'): R --> \
   16.64  \            mk_trace C`ex = mk_trace A`((corresp_ex_simC A R`ex) s')";
   16.65  
   16.66 @@ -188,7 +188,7 @@
   16.67  
   16.68  
   16.69  Goal 
   16.70 - "!!f.[| is_simulation R C A |] ==>\
   16.71 + "[| is_simulation R C A |] ==>\
   16.72  \ !s s'. reachable C s & is_exec_frag C (s,ex) & (s,s'):R  \
   16.73  \ --> is_exec_frag A (s',(corresp_ex_simC A R`ex) s')"; 
   16.74  
   16.75 @@ -240,7 +240,7 @@
   16.76       S':= @s'. (s,s'):R & s':starts_of A, where s:starts_of C  *)
   16.77  
   16.78  Goal 
   16.79 -"!!C. [| is_simulation R C A; s:starts_of C |] \
   16.80 +"[| is_simulation R C A; s:starts_of C |] \
   16.81  \ ==> let S' = @s'. (s,s'):R & s':starts_of A in \
   16.82  \     (s,S'):R & S':starts_of A";
   16.83    by (asm_full_simp_tac (simpset() addsimps [is_simulation_def,
   16.84 @@ -259,7 +259,7 @@
   16.85  
   16.86  
   16.87  Goalw [traces_def]
   16.88 -  "!!f. [| ext C = ext A; is_simulation R C A |] \
   16.89 +  "[| ext C = ext A; is_simulation R C A |] \
   16.90  \          ==> traces C <= traces A"; 
   16.91  
   16.92    by (simp_tac(simpset() addsimps [has_trace_def2])1);
    17.1 --- a/src/HOLCF/IOA/meta_theory/TL.ML	Thu Jan 28 18:28:06 1999 +0100
    17.2 +++ b/src/HOLCF/IOA/meta_theory/TL.ML	Fri Jan 29 16:23:56 1999 +0100
    17.3 @@ -50,7 +50,7 @@
    17.4  qed"reflT";
    17.5  
    17.6  
    17.7 -Goal "!!x. [| suffix y x ; suffix z y |]  ==> suffix z x";
    17.8 +Goal "[| suffix y x ; suffix z y |]  ==> suffix z x";
    17.9  by (asm_full_simp_tac (simpset() addsimps [suffix_def])1);
   17.10  by Auto_tac;
   17.11  by (res_inst_tac [("x","s1 @@ s1a")] exI 1);
   17.12 @@ -79,21 +79,21 @@
   17.13  (*                      TLA Rules by Lamport                        *)
   17.14  (* ---------------------------------------------------------------- *)
   17.15  
   17.16 -Goal "!! P. validT P ==> validT ([] P)";
   17.17 +Goal "validT P ==> validT ([] P)";
   17.18  by (asm_full_simp_tac (simpset() addsimps [validT_def,satisfies_def,Box_def,tsuffix_def])1);
   17.19  qed"STL1a";
   17.20  
   17.21 -Goal "!! P. valid P ==> validT (Init P)";
   17.22 +Goal "valid P ==> validT (Init P)";
   17.23  by (asm_full_simp_tac (simpset() addsimps [valid_def,validT_def,satisfies_def,Init_def])1);
   17.24  qed"STL1b";
   17.25  
   17.26 -Goal "!! P. valid P ==> validT ([] (Init P))";
   17.27 +Goal "valid P ==> validT ([] (Init P))";
   17.28  by (rtac STL1a 1);
   17.29  by (etac STL1b 1);
   17.30  qed"STL1";
   17.31  
   17.32  (* Note that unlift and HD is not at all used !!! *)
   17.33 -Goal "!! P. valid (P .--> Q)  ==> validT ([] (Init P) .--> [] (Init Q))";
   17.34 +Goal "valid (P .--> Q)  ==> validT ([] (Init P) .--> [] (Init Q))";
   17.35  by (asm_full_simp_tac (simpset() addsimps [valid_def,validT_def,satisfies_def,IMPLIES_def,Box_def,Init_def])1);
   17.36  qed"STL4";
   17.37  
   17.38 @@ -158,11 +158,11 @@
   17.39  
   17.40  
   17.41  
   17.42 -Goal "!! P. [| validT (P .--> Q); validT P |] ==> validT Q";
   17.43 +Goal "[| validT (P .--> Q); validT P |] ==> validT Q";
   17.44  by (asm_full_simp_tac (simpset() addsimps [validT_def,satisfies_def,IMPLIES_def])1);
   17.45  qed"ModusPonens";
   17.46  
   17.47  (* works only if validT is defined without restriction to s~=UU, s~=nil *)
   17.48 -Goal "!! P. validT P ==> validT (Next P)";
   17.49 +Goal "validT P ==> validT (Next P)";
   17.50  by (asm_full_simp_tac (simpset() addsimps [validT_def,satisfies_def,Next_def])1);
   17.51  (* qed"NextTauto"; *)
    18.1 --- a/src/HOLCF/IOA/meta_theory/TLS.ML	Thu Jan 28 18:28:06 1999 +0100
    18.2 +++ b/src/HOLCF/IOA/meta_theory/TLS.ML	Fri Jan 29 16:23:56 1999 +0100
    18.3 @@ -86,21 +86,21 @@
    18.4     after the translation via ex2seq !! *)
    18.5  
    18.6  Goalw [Init_def,Next_def,temp_sat_def,satisfies_def,IMPLIES_def,AND_def]
    18.7 - "!! A. [| ! s a t. (P s) & s-a--A-> t --> (Q t) |]\
    18.8 + "[| ! s a t. (P s) & s-a--A-> t --> (Q t) |]\
    18.9  \  ==> ex |== (Init (%(s,a,t). P s) .& Init (%(s,a,t). s -a--A-> t) \
   18.10  \             .--> (Next (Init (%(s,a,t).Q s))))";
   18.11  
   18.12  by (clarify_tac set_cs 1);
   18.13  by (asm_full_simp_tac (simpset() setloop split_tac [expand_if]) 1);
   18.14  (* TL = UU *)
   18.15 -br conjI 1;
   18.16 +by (rtac conjI 1);
   18.17  by (pair_tac "ex" 1);
   18.18  by (Seq_case_simp_tac "y" 1);
   18.19  by (pair_tac "a" 1);
   18.20  by (Seq_case_simp_tac "s" 1);
   18.21  by (pair_tac "a" 1);
   18.22  (* TL = nil *)
   18.23 -br conjI 1;
   18.24 +by (rtac conjI 1);
   18.25  by (pair_tac "ex" 1);
   18.26  by (Seq_case_simp_tac "y" 1);
   18.27  by (asm_full_simp_tac (simpset() addsimps [unlift_def])1);