# HG changeset patch
# User paulson
# Date 917623436 -3600
# Node ID bc2a76ce1ea3454850820ccc5afdf1ce64a69968
# Parent  32c0b8f57bb7523f2bd3b51adf9082eaff9583b7
tidied

diff -r 32c0b8f57bb7 -r bc2a76ce1ea3 src/HOL/UNITY/Lift.ML
--- a/src/HOL/UNITY/Lift.ML	Thu Jan 28 18:28:06 1999 +0100
+++ b/src/HOL/UNITY/Lift.ML	Fri Jan 29 16:23:56 1999 +0100
@@ -37,7 +37,6 @@
 (*The order in which they are applied seems to be critical...*)
 val mov_metrics = [mov_metric2, mov_metric3, mov_metric1, mov_metric4];
 
-
 val metric_simps = [metric_def, vimage_def];
 
 
@@ -109,7 +108,7 @@
 by (constrains_tac 1);
 by (ALLGOALS Clarify_tac);
 by (REPEAT_FIRST distinct_tac);
-by (ALLGOALS (asm_simp_tac (simpset() addsimps [zle_imp_zle_zadd])));
+by Auto_tac;
 qed "bounded";
 
 
@@ -246,8 +245,6 @@
 by Auto_tac;
 by (REPEAT_FIRST (eresolve_tac mov_metrics));
 by (ALLGOALS (asm_simp_tac (simpset() addsimps metric_simps @ zcompare_rls)));
-(** LEVEL 5 **)
-by (dres_inst_tac [("w1","Min")] (zle_iff_zadd RS iffD1) 1);
 by (Blast_tac 1);
 qed "E_thm16a";
 
@@ -260,8 +257,6 @@
 by Auto_tac;
 by (REPEAT_FIRST (eresolve_tac mov_metrics));
 by (ALLGOALS (asm_simp_tac (simpset() addsimps metric_simps @ zcompare_rls)));
-(** LEVEL 5 **)
-by (dres_inst_tac [("z1","Max")] (zle_iff_zadd RS iffD1) 1);
 by (Blast_tac 1);
 qed "E_thm16b";
 
diff -r 32c0b8f57bb7 -r bc2a76ce1ea3 src/HOLCF/IOA/Storage/Correctness.ML
--- a/src/HOLCF/IOA/Storage/Correctness.ML	Thu Jan 28 18:28:06 1999 +0100
+++ b/src/HOLCF/IOA/Storage/Correctness.ML	Fri Jan 29 16:23:56 1999 +0100
@@ -28,7 +28,7 @@
 (* ---------------- main-part ------------------- *)
 
 by (REPEAT (rtac allI 1));
-br imp_conj_lemma 1;
+by (rtac imp_conj_lemma 1);
 ren "k b used c k' b' a" 1;
 by (induct_tac "a" 1);
 by (ALLGOALS (simp_tac (simpset() addsimps [sim_relation_def,
@@ -37,13 +37,13 @@
 (* NEW *)
 by (res_inst_tac [("x","(used,True)")] exI 1);
 by (Asm_full_simp_tac 1);
-br transition_is_ex 1;
+by (rtac transition_is_ex 1);
 by (simp_tac (simpset() addsimps [
       Spec.ioa_def,Spec.trans_def,trans_of_def])1);
 (* LOC *)
 by (res_inst_tac [("x","(used Un {k},False)")] exI 1);
 by (Asm_full_simp_tac 1);
-br transition_is_ex 1;
+by (rtac transition_is_ex 1);
 by (simp_tac (simpset() addsimps [
       Spec.ioa_def,Spec.trans_def,trans_of_def])1);
 by (Fast_tac 1);
@@ -51,8 +51,8 @@
 by (res_inst_tac [("x","(used - {nat},c)")] exI 1);
 by (Asm_full_simp_tac 1);
 by (SELECT_GOAL (safe_tac set_cs) 1);
-auto();
-br transition_is_ex 1;
+by Auto_tac;
+by (rtac transition_is_ex 1);
 by (simp_tac (simpset() addsimps [
       Spec.ioa_def,Spec.trans_def,trans_of_def])1);
 qed"issimulation";
@@ -61,14 +61,14 @@
 
 Goalw [ioa_implements_def] 
 "impl_ioa =<| spec_ioa";
-br conjI 1;
+by (rtac conjI 1);
 by (simp_tac (simpset() addsimps [Impl.sig_def,Spec.sig_def,
     Impl.ioa_def,Spec.ioa_def, asig_outputs_def,asig_of_def,
     asig_inputs_def]) 1);
-br trace_inclusion_for_simulations 1;
+by (rtac trace_inclusion_for_simulations 1);
 by (simp_tac (simpset() addsimps [Impl.sig_def,Spec.sig_def,
     Impl.ioa_def,Spec.ioa_def, externals_def,asig_outputs_def,asig_of_def,
     asig_inputs_def]) 1);
-br issimulation 1;
+by (rtac issimulation 1);
 qed"implementation";
 
diff -r 32c0b8f57bb7 -r bc2a76ce1ea3 src/HOLCF/IOA/meta_theory/Abstraction.ML
--- a/src/HOLCF/IOA/meta_theory/Abstraction.ML	Thu Jan 28 18:28:06 1999 +0100
+++ b/src/HOLCF/IOA/meta_theory/Abstraction.ML	Fri Jan 29 16:23:56 1999 +0100
@@ -57,7 +57,7 @@
 
 
 Goalw [cex_abs_def]
- "!!h.[| is_abstraction h C A |] ==>\
+ "[| is_abstraction h C A |] ==>\
 \ !s. reachable C s & is_exec_frag C (s,xs) \
 \ --> is_exec_frag A (cex_abs h (s,xs))"; 
 
@@ -72,7 +72,7 @@
 qed_spec_mp"exec_frag_abstraction";
 
 
-Goal "!!A. is_abstraction h C A ==> weakeningIOA A C h";
+Goal "is_abstraction h C A ==> weakeningIOA A C h";
 by (asm_full_simp_tac (simpset() addsimps [weakeningIOA_def])1);
 by Auto_tac;
 by (asm_full_simp_tac (simpset() addsimps [executions_def]) 1);
@@ -85,7 +85,7 @@
 qed"abs_is_weakening";
 
 
-Goal "!!A. [|is_abstraction h C A; validIOA A Q; temp_strengthening Q P h |] \
+Goal "[|is_abstraction h C A; validIOA A Q; temp_strengthening Q P h |] \
 \         ==> validIOA C P";
 by (dtac abs_is_weakening 1);
 by (asm_full_simp_tac (simpset() addsimps [weakeningIOA_def, 
@@ -117,7 +117,7 @@
 
 
 Goalw [is_live_abstraction_def]
-   "!!A. [|is_live_abstraction h (C,L) (A,M); \
+   "[|is_live_abstraction h (C,L) (A,M); \
 \         validLIOA (A,M) Q;  temp_strengthening Q P h |] \
 \         ==> validLIOA (C,L) P";
 by Auto_tac;
@@ -130,7 +130,7 @@
 
 
 Goalw [is_live_abstraction_def]
-   "!!A. [|is_live_abstraction h (C,L) (A,M); \
+   "[|is_live_abstraction h (C,L) (A,M); \
 \         validLIOA (A,M) (H1 .--> Q);  temp_strengthening Q P h; \
 \         temp_weakening H1 H2 h; validLIOA (C,L) H2 |] \
 \         ==> validLIOA (C,L) P";
@@ -151,14 +151,14 @@
 
 
 Goalw [is_abstraction_def,is_ref_map_def] 
-"!! h. is_abstraction h C A ==> is_ref_map h C A";
+"is_abstraction h C A ==> is_ref_map h C A";
 by (safe_tac set_cs);
 by (res_inst_tac[("x","(a,h t)>>nil")] exI 1);
 by (asm_full_simp_tac (simpset() addsimps [move_def])1);
 qed"abstraction_is_ref_map";
 
 
-Goal "!! h. [| inp(C)=inp(A); out(C)=out(A); \
+Goal "[| inp(C)=inp(A); out(C)=out(A); \
 \                  is_abstraction h C A |] \
 \               ==> C =<| A";
 by (asm_full_simp_tac (simpset() addsimps [ioa_implements_def]) 1);
@@ -179,7 +179,7 @@
 (* Reduces to Filter (Map fst x) = Filter (Map fst (Map (%(a,t). (a,x)) x),
    that is to special Map Lemma *)
 Goalw [cex_abs_def,mk_trace_def,filter_act_def]
-  "!! f. ext C = ext A \
+  "ext C = ext A \
 \        ==> mk_trace C`xs = mk_trace A`(snd (cex_abs f (s,xs)))";
 by (Asm_full_simp_tac 1);
 by (pair_induct_tac "xs" [] 1);
@@ -190,7 +190,7 @@
    is_live_abstraction includes temp_strengthening which is necessarily based
    on cex_abs and not on corresp_ex. Thus, the proof is redoone in a more specific
    way for cex_abs *)
-Goal "!! h. [| inp(C)=inp(A); out(C)=out(A); \
+Goal "[| inp(C)=inp(A); out(C)=out(A); \
 \                  is_live_abstraction h (C,M) (A,L) |] \
 \               ==> live_implements (C,M) (A,L)";
 
@@ -223,7 +223,7 @@
 (* FIX: NAch Traces.ML bringen *)
 
 Goalw [ioa_implements_def] 
-"!! A. [| A =<| B; B =<| C|] ==> A =<| C"; 
+"[| A =<| B; B =<| C|] ==> A =<| C"; 
 by Auto_tac;
 qed"implements_trans";
 
@@ -234,7 +234,7 @@
 (*                Abstraction Rules for Automata                    *)
 (* ---------------------------------------------------------------- *)
 
-Goal "!! C. [| inp(C)=inp(A); out(C)=out(A); \
+Goal "[| inp(C)=inp(A); out(C)=out(A); \
 \                  inp(Q)=inp(P); out(Q)=out(P); \
 \                  is_abstraction h1 C A; \
 \                  A =<| Q ; \
@@ -250,7 +250,7 @@
 qed"AbsRuleA1";
 
 
-Goal "!! C. [| inp(C)=inp(A); out(C)=out(A); \
+Goal "[| inp(C)=inp(A); out(C)=out(A); \
 \                  inp(Q)=inp(P); out(Q)=out(P); \
 \                  is_live_abstraction h1 (C,LC) (A,LA); \
 \                  live_implements (A,LA) (Q,LQ) ; \
@@ -276,28 +276,28 @@
 (* ---------------------------------------------------------------- *)
 
 Goalw [temp_strengthening_def]
-"!! h. [| temp_strengthening P1 Q1 h; \
+"[| temp_strengthening P1 Q1 h; \
 \         temp_strengthening P2 Q2 h |] \
 \      ==> temp_strengthening (P1 .& P2) (Q1 .& Q2) h";
 by Auto_tac;
 qed"strength_AND";
 
 Goalw [temp_strengthening_def]
-"!! h. [| temp_strengthening P1 Q1 h; \
+"[| temp_strengthening P1 Q1 h; \
 \         temp_strengthening P2 Q2 h |] \
 \      ==> temp_strengthening (P1 .| P2) (Q1 .| Q2) h";
 by Auto_tac;
 qed"strength_OR";
 
 Goalw [temp_strengthening_def]
-"!! h. [| temp_weakening P Q h |] \
+"[| temp_weakening P Q h |] \
 \      ==> temp_strengthening (.~ P) (.~ Q) h";
 by (asm_full_simp_tac (simpset() addsimps [temp_weakening_def2])1);
 by Auto_tac;
 qed"strength_NOT";
 
 Goalw [temp_strengthening_def]
-"!! h. [| temp_weakening P1 Q1 h; \
+"[| temp_weakening P1 Q1 h; \
 \         temp_strengthening P2 Q2 h |] \
 \      ==> temp_strengthening (P1 .--> P2) (Q1 .--> Q2) h";
 by (asm_full_simp_tac (simpset() addsimps [temp_weakening_def2])1);
@@ -310,28 +310,28 @@
 (* ---------------------------------------------------------------- *)
 
 Goal
-"!! h. [| temp_weakening P1 Q1 h; \
+"[| temp_weakening P1 Q1 h; \
 \         temp_weakening P2 Q2 h |] \
 \      ==> temp_weakening (P1 .& P2) (Q1 .& Q2) h";
 by (asm_full_simp_tac (simpset() addsimps [temp_weakening_def2])1);
 qed"weak_AND";
 
 Goal 
-"!! h. [| temp_weakening P1 Q1 h; \
+"[| temp_weakening P1 Q1 h; \
 \         temp_weakening P2 Q2 h |] \
 \      ==> temp_weakening (P1 .| P2) (Q1 .| Q2) h";
 by (asm_full_simp_tac (simpset() addsimps [temp_weakening_def2])1);
 qed"weak_OR";
 
 Goalw [temp_strengthening_def]
-"!! h. [| temp_strengthening P Q h |] \
+"[| temp_strengthening P Q h |] \
 \      ==> temp_weakening (.~ P) (.~ Q) h";
 by (asm_full_simp_tac (simpset() addsimps [temp_weakening_def2])1);
 by Auto_tac;
 qed"weak_NOT";
 
 Goalw [temp_strengthening_def]
-"!! h. [| temp_strengthening P1 Q1 h; \
+"[| temp_strengthening P1 Q1 h; \
 \         temp_weakening P2 Q2 h |] \
 \      ==> temp_weakening (P1 .--> P2) (Q1 .--> Q2) h";
 by (asm_full_simp_tac (simpset() addsimps [temp_weakening_def2])1);
@@ -373,7 +373,7 @@
 (* important property of ex2seq: can be shiftet, as defined "pointwise" *)
 
 Goalw [tsuffix_def,suffix_def]
-"!!s. tsuffix s (ex2seq ex) ==> ? ex'. s = (ex2seq ex')";
+"tsuffix s (ex2seq ex) ==> ? ex'. s = (ex2seq ex')";
 by Auto_tac;
 by (dtac ex2seqConc 1);
 by Auto_tac;
@@ -395,7 +395,7 @@
   properties carry over *)
 
 Goalw [tsuffix_def,suffix_def,cex_absSeq_def]
-"!! s. tsuffix s t ==> tsuffix (cex_absSeq h s) (cex_absSeq h t)";
+"tsuffix s t ==> tsuffix (cex_absSeq h s) (cex_absSeq h t)";
 by Auto_tac;
 by (asm_full_simp_tac (simpset() addsimps [Mapnil])1);
 by (asm_full_simp_tac (simpset() addsimps [MapUU])1);
@@ -406,7 +406,7 @@
 
 Goalw [temp_strengthening_def,state_strengthening_def, temp_sat_def,
 satisfies_def,Box_def]
-"!! h. [| temp_strengthening P Q h |]\
+"[| temp_strengthening P Q h |]\
 \      ==> temp_strengthening ([] P) ([] Q) h";
 by (clarify_tac set_cs 1);
 by (forward_tac [ex2seq_tsuffix] 1);
@@ -420,7 +420,7 @@
 
 Goalw [temp_strengthening_def,state_strengthening_def,
 temp_sat_def,satisfies_def,Init_def,unlift_def]
-"!! h. [| state_strengthening P Q h |]\
+"[| state_strengthening P Q h |]\
 \      ==> temp_strengthening (Init P) (Init Q) h";
 by (safe_tac set_cs);
 by (pair_tac "ex" 1);
@@ -464,7 +464,7 @@
 
 (* important property of ex2seq: can be shiftet, as defined "pointwise" *)
 
-Goal "!!ex. [| (snd ex)~=UU ; (snd ex)~=nil |] ==> (? ex'. TL`(ex2seq ex) = ex2seq ex')";
+Goal "[| (snd ex)~=UU ; (snd ex)~=nil |] ==> (? ex'. TL`(ex2seq ex) = ex2seq ex')";
 by (pair_tac "ex" 1);
 by (Seq_case_simp_tac "y" 1);
 by (pair_tac "a" 1);
@@ -483,7 +483,7 @@
 
 Goalw [temp_strengthening_def,state_strengthening_def,
 temp_sat_def, satisfies_def,Next_def]
-"!! h. [| temp_strengthening P Q h |]\
+"[| temp_strengthening P Q h |]\
 \      ==> temp_strengthening (Next P) (Next Q) h";
 by (Asm_full_simp_tac 1);
 by (safe_tac set_cs);
@@ -494,7 +494,7 @@
 (* cons case *)
 by (asm_full_simp_tac (simpset() addsimps [TL_ex2seq_nil,TL_ex2seq_UU,
         ex2seq_abs_cex,cex_absSeq_TL RS sym, ex2seqnilTL])1);
-be conjE 1;
+by (etac conjE 1);
 by (dtac TLex2seq 1);
 by (assume_tac 1);
 by Auto_tac;
@@ -508,7 +508,7 @@
 
 
 Goal 
-"!! h. [| state_weakening P Q h |]\
+"[| state_weakening P Q h |]\
 \      ==> temp_weakening (Init P) (Init Q) h";
 by (asm_full_simp_tac (simpset() addsimps [temp_weakening_def2,
       state_weakening_def2, temp_sat_def,satisfies_def,Init_def,unlift_def])1);
@@ -525,7 +525,7 @@
 
 
 Goalw [Diamond_def]
-"!! h. [| temp_strengthening P Q h |]\
+"[| temp_strengthening P Q h |]\
 \      ==> temp_strengthening (<> P) (<> Q) h";
 by (rtac strength_NOT 1);
 by (rtac weak_Box 1);
@@ -533,7 +533,7 @@
 qed"strength_Diamond";
 
 Goalw [Leadsto_def]
-"!! h. [| temp_weakening P1 P2 h;\
+"[| temp_weakening P1 P2 h;\
 \         temp_strengthening Q1 Q2 h |]\
 \      ==> temp_strengthening (P1 ~> Q1) (P2 ~> Q2) h";
 by (rtac strength_Box 1);
@@ -548,7 +548,7 @@
 
 
 Goalw [Diamond_def]
-"!! h. [| temp_weakening P Q h |]\
+"[| temp_weakening P Q h |]\
 \      ==> temp_weakening (<> P) (<> Q) h";
 by (rtac weak_NOT 1);
 by (rtac strength_Box 1);
@@ -556,7 +556,7 @@
 qed"weak_Diamond";
 
 Goalw [Leadsto_def]
-"!! h. [| temp_strengthening P1 P2 h;\
+"[| temp_strengthening P1 P2 h;\
 \         temp_weakening Q1 Q2 h |]\
 \      ==> temp_weakening (P1 ~> Q1) (P2 ~> Q2) h";
 by (rtac weak_Box 1);
diff -r 32c0b8f57bb7 -r bc2a76ce1ea3 src/HOLCF/IOA/meta_theory/Asig.ML
--- a/src/HOLCF/IOA/meta_theory/Asig.ML	Thu Jan 28 18:28:06 1999 +0100
+++ b/src/HOLCF/IOA/meta_theory/Asig.ML	Fri Jan 29 16:23:56 1999 +0100
@@ -6,8 +6,6 @@
 Action signatures
 *)
 
-open Asig;
-
 val asig_projections = [asig_inputs_def, asig_outputs_def, asig_internals_def];
 
 Goal
@@ -17,23 +15,23 @@
   by (simp_tac (simpset() addsimps asig_projections) 1);
 qed "asig_triple_proj";
 
-Goal "!!a.[| a~:internals(S) ;a~:externals(S)|] ==> a~:actions(S)";
+Goal "[| a~:internals(S) ;a~:externals(S)|] ==> a~:actions(S)";
 by (asm_full_simp_tac (simpset() addsimps [externals_def,actions_def]) 1);
 qed"int_and_ext_is_act";
 
-Goal "!!a.[|a:externals(S)|] ==> a:actions(S)";
+Goal "[|a:externals(S)|] ==> a:actions(S)";
 by (asm_full_simp_tac (simpset() addsimps [externals_def,actions_def]) 1);
 qed"ext_is_act";
 
-Goal "!!a.[|a:internals S|] ==> a:actions S";
+Goal "[|a:internals S|] ==> a:actions S";
 by (asm_full_simp_tac (simpset() addsimps [asig_internals_def,actions_def]) 1);
 qed"int_is_act";
 
-Goal "!!a.[|a:inputs S|] ==> a:actions S";
+Goal "[|a:inputs S|] ==> a:actions S";
 by (asm_full_simp_tac (simpset() addsimps [asig_inputs_def,actions_def]) 1);
 qed"inp_is_act";
 
-Goal "!!a.[|a:outputs S|] ==> a:actions S";
+Goal "[|a:outputs S|] ==> a:actions S";
 by (asm_full_simp_tac (simpset() addsimps [asig_outputs_def,actions_def]) 1);
 qed"out_is_act";
 
@@ -41,19 +39,19 @@
 by (fast_tac (claset() addSIs [ext_is_act]) 1 );
 qed"ext_and_act";
  
-Goal "!!S. [|is_asig S;x: actions S|] ==> (x~:externals S) = (x: internals S)";
+Goal "[|is_asig S;x: actions S|] ==> (x~:externals S) = (x: internals S)";
 by (asm_full_simp_tac (simpset() addsimps [actions_def,is_asig_def,externals_def]) 1);
-by (best_tac (set_cs addEs [equalityCE]) 1);
+by (Blast_tac 1);
 qed"not_ext_is_int";
 
-Goal "!!S. is_asig S ==> (x~:externals S) = (x: internals S | x~:actions S)";
+Goal "is_asig S ==> (x~:externals S) = (x: internals S | x~:actions S)";
 by (asm_full_simp_tac (simpset() addsimps [actions_def,is_asig_def,externals_def]) 1);
-by (best_tac (set_cs addEs [equalityCE]) 1);
+by (Blast_tac 1);
 qed"not_ext_is_int_or_not_act";
 
 Goalw  [externals_def,actions_def,is_asig_def]
- "!! x. [| is_asig (S); x:internals S |] ==> x~:externals S";
+ "[| is_asig (S); x:internals S |] ==> x~:externals S";
 by (Asm_full_simp_tac 1);
-by (best_tac (set_cs addEs [equalityCE]) 1);
+by (Blast_tac 1);
 qed"int_is_not_ext";
 
diff -r 32c0b8f57bb7 -r bc2a76ce1ea3 src/HOLCF/IOA/meta_theory/Automata.ML
--- a/src/HOLCF/IOA/meta_theory/Automata.ML	Thu Jan 28 18:28:06 1999 +0100
+++ b/src/HOLCF/IOA/meta_theory/Automata.ML	Fri Jan 29 16:23:56 1999 +0100
@@ -9,12 +9,9 @@
 (* this modification of the simpset is local to this file *)
 Delsimps [split_paired_Ex];
 
-
-open reachable;
-
 val ioa_projections = [asig_of_def, starts_of_def, trans_of_def,wfair_of_def,sfair_of_def];
 
-(* ----------------------------------------------------------------------------------- *)
+(* ------------------------------------------------------------------------- *)
 
 section "asig_of, starts_of, trans_of";
 
@@ -29,7 +26,7 @@
 qed "ioa_triple_proj";
 
 Goalw [is_trans_of_def,actions_def, is_asig_def]
-  "!!A. [| is_trans_of A; (s1,a,s2):trans_of(A) |] ==> a:act A";
+  "[| is_trans_of A; (s1,a,s2):trans_of(A) |] ==> a:act A";
   by (REPEAT(etac conjE 1));
   by (EVERY1[etac allE, etac impE, atac]);
   by (Asm_full_simp_tac 1);
@@ -55,7 +52,7 @@
 qed "trans_of_par";
 
 
-(* ----------------------------------------------------------------------------------- *)
+(* ------------------------------------------------------------------------- *)
 
 section "actions and par";
 
@@ -107,7 +104,7 @@
       asig_inputs_def,asig_outputs_def,asig_internals_def,Un_def,set_diff_def]) 1);
 qed"internals_of_par";
 
-(* ---------------------------------------------------------------------------------- *)
+(* ------------------------------------------------------------------------ *)
 
 section "actions and compatibility"; 
 
@@ -117,50 +114,50 @@
 qed"compat_commute";
 
 Goalw [externals_def,actions_def,compatible_def]
- "!! a. [| compatible A1 A2; a:ext A1|] ==> a~:int A2";
+ "[| compatible A1 A2; a:ext A1|] ==> a~:int A2";
 by (Asm_full_simp_tac 1);
-by (best_tac (set_cs addEs [equalityCE]) 1);
+by (Blast_tac 1);
 qed"ext1_is_not_int2";
 
 (* just commuting the previous one: better commute compatible *)
 Goalw [externals_def,actions_def,compatible_def]
- "!! a. [| compatible A2 A1 ; a:ext A1|] ==> a~:int A2";
+ "[| compatible A2 A1 ; a:ext A1|] ==> a~:int A2";
 by (Asm_full_simp_tac 1);
-by (best_tac (set_cs addEs [equalityCE]) 1);
+by (Blast_tac 1);
 qed"ext2_is_not_int1";
 
 bind_thm("ext1_ext2_is_not_act2",ext1_is_not_int2 RS int_and_ext_is_act);
 bind_thm("ext1_ext2_is_not_act1",ext2_is_not_int1 RS int_and_ext_is_act);
 
 Goalw  [externals_def,actions_def,compatible_def]
- "!! x. [| compatible A B; x:int A |] ==> x~:ext B";
+ "[| compatible A B; x:int A |] ==> x~:ext B";
 by (Asm_full_simp_tac 1);
-by (best_tac (set_cs addEs [equalityCE]) 1);
+by (Blast_tac 1);
 qed"intA_is_not_extB";
 
 Goalw [externals_def,actions_def,compatible_def,is_asig_def,asig_of_def]
-"!! a. [| compatible A B; a:int A |] ==> a ~: act B";
+"[| compatible A B; a:int A |] ==> a ~: act B";
 by (Asm_full_simp_tac 1);
-by (best_tac (set_cs addEs [equalityCE]) 1);
+by (Blast_tac 1);
 qed"intA_is_not_actB";
 
 (* the only one that needs disjointness of outputs and of internals and _all_ acts *)
 Goalw [asig_outputs_def,asig_internals_def,actions_def,asig_inputs_def,
     compatible_def,is_asig_def,asig_of_def]
-"!! a. [| compatible A B; a:out A ;a:act B|] ==> a : inp B";
+"[| compatible A B; a:out A ;a:act B|] ==> a : inp B";
 by (Asm_full_simp_tac 1);
-by (best_tac (set_cs addEs [equalityCE]) 1);
+by (Blast_tac 1);
 qed"outAactB_is_inpB";
 
 (* needed for propagation of input_enabledness from A,B to A||B *)
 Goalw [asig_outputs_def,asig_internals_def,actions_def,asig_inputs_def,
     compatible_def,is_asig_def,asig_of_def]
-"!! a. [| compatible A B; a:inp A ;a:act B|] ==> a : inp B | a: out B";
+"[| compatible A B; a:inp A ;a:act B|] ==> a : inp B | a: out B";
 by (Asm_full_simp_tac 1);
-by (best_tac (set_cs addEs [equalityCE]) 1);
+by (Blast_tac 1);
 qed"inpAAactB_is_inpBoroutB";
 
-(* ---------------------------------------------------------------------------------- *)
+(* ------------------------------------------------------------------------- *)
 
 section "input_enabledness and par";  
 
@@ -169,7 +166,7 @@
      1. inpAAactB_is_inpBoroutB ie. internals are really hidden.
      2. inputs_of_par: outputs are no longer inputs of par. This is important here *)
 Goalw [input_enabled_def] 
-"!!A. [| compatible A B; input_enabled A; input_enabled B|] \
+"[| compatible A B; input_enabled A; input_enabled B|] \
 \     ==> input_enabled (A||B)";
 by (asm_full_simp_tac (simpset()addsimps[Let_def,inputs_of_par,trans_of_par])1);
 by (safe_tac set_cs);
@@ -232,7 +229,7 @@
 by (Asm_full_simp_tac 1);
 qed"input_enabled_par";
 
-(* ---------------------------------------------------------------------------------- *)
+(* ------------------------------------------------------------------------- *)
 
 section "invariants";
 
@@ -252,21 +249,23 @@
 
 val [p1,p2] = goal thy
  "[| !!s. s : starts_of(A) ==> P(s); \
-\   !!s t a. reachable A s ==> P(s) --> (s,a,t):trans_of(A) --> P(t) \
+\    !!s t a. reachable A s ==> P(s) --> (s,a,t):trans_of(A) --> P(t) \
 \ |] ==> invariant A P";
   by (fast_tac (HOL_cs addSIs [invariantI] addSDs [p1,p2]) 1);
 qed "invariantI1";
 
-val [p1,p2] = goalw thy [invariant_def]
-"[| invariant A P; reachable A s |] ==> P(s)";
-   br(p2 RS (p1 RS spec RS mp))1;
+Goalw [invariant_def] "[| invariant A P; reachable A s |] ==> P(s)";
+by (Blast_tac 1);   
 qed "invariantE";
 
-(* ---------------------------------------------------------------------------------- *)
+(* ------------------------------------------------------------------------- *)
 
 section "restrict";
 
 
+val reachable_0 = reachable.reachable_0
+and reachable_n = reachable.reachable_n;
+
 Goal "starts_of(restrict ioa acts) = starts_of(ioa) &     \
 \         trans_of(restrict ioa acts) = trans_of(ioa)";
 by (simp_tac (simpset() addsimps ([restrict_def]@ioa_projections)) 1);
@@ -300,18 +299,18 @@
   by (simp_tac (simpset() addsimps [cancel_restrict_a,cancel_restrict_b,acts_restrict]) 1);
 qed"cancel_restrict";
 
-(* ---------------------------------------------------------------------------------- *)
+(* ------------------------------------------------------------------------- *)
 
 section "rename";
 
 
 
-Goal "!!f. s -a--(rename C f)-> t ==> (? x. Some(x) = f(a) & s -x--C-> t)";
+Goal "s -a--(rename C f)-> t ==> (? x. Some(x) = f(a) & s -x--C-> t)";
 by (asm_full_simp_tac (simpset() addsimps [Let_def,rename_def,trans_of_def]) 1);
 qed"trans_rename";
 
 
-Goal "!!s.[| reachable (rename C g) s |] ==> reachable C s";
+Goal "[| reachable (rename C g) s |] ==> reachable C s";
 by (etac reachable.induct 1);
 by (rtac reachable_0 1);
 by (asm_full_simp_tac (simpset() addsimps [rename_def]@ioa_projections) 1);
@@ -324,49 +323,49 @@
 
 
 
-(* ---------------------------------------------------------------------------------- *)
+(* ------------------------------------------------------------------------- *)
 
 section "trans_of(A||B)";
 
 
-Goal "!!A.[|(s,a,t):trans_of (A||B); a:act A|] \
+Goal "[|(s,a,t):trans_of (A||B); a:act A|] \
 \             ==> (fst s,a,fst t):trans_of A";
 by (asm_full_simp_tac (simpset() addsimps [Let_def,par_def,trans_of_def]) 1);
 qed"trans_A_proj";
 
-Goal "!!A.[|(s,a,t):trans_of (A||B); a:act B|] \
+Goal "[|(s,a,t):trans_of (A||B); a:act B|] \
 \             ==> (snd s,a,snd t):trans_of B";
 by (asm_full_simp_tac (simpset() addsimps [Let_def,par_def,trans_of_def]) 1);
 qed"trans_B_proj";
 
-Goal "!!A.[|(s,a,t):trans_of (A||B); a~:act A|]\
+Goal "[|(s,a,t):trans_of (A||B); a~:act A|]\
 \             ==> fst s = fst t";
 by (asm_full_simp_tac (simpset() addsimps [Let_def,par_def,trans_of_def]) 1);
 qed"trans_A_proj2";
 
-Goal "!!A.[|(s,a,t):trans_of (A||B); a~:act B|]\
+Goal "[|(s,a,t):trans_of (A||B); a~:act B|]\
 \             ==> snd s = snd t";
 by (asm_full_simp_tac (simpset() addsimps [Let_def,par_def,trans_of_def]) 1);
 qed"trans_B_proj2";
 
-Goal "!!A.(s,a,t):trans_of (A||B) \
+Goal "(s,a,t):trans_of (A||B) \
 \              ==> a :act A | a :act B";
 by (asm_full_simp_tac (simpset() addsimps [Let_def,par_def,trans_of_def]) 1);
 qed"trans_AB_proj";
 
-Goal "!!A. [|a:act A;a:act B;\
+Goal "[|a:act A;a:act B;\
 \      (fst s,a,fst t):trans_of A;(snd s,a,snd t):trans_of B|]\
 \  ==> (s,a,t):trans_of (A||B)";
 by (asm_full_simp_tac (simpset() addsimps [Let_def,par_def,trans_of_def]) 1);
 qed"trans_AB";
 
-Goal "!!A. [|a:act A;a~:act B;\
+Goal "[|a:act A;a~:act B;\
 \      (fst s,a,fst t):trans_of A;snd s=snd t|]\
 \  ==> (s,a,t):trans_of (A||B)";
 by (asm_full_simp_tac (simpset() addsimps [Let_def,par_def,trans_of_def]) 1);
 qed"trans_A_notB";
 
-Goal "!!A. [|a~:act A;a:act B;\
+Goal "[|a~:act A;a:act B;\
 \      (snd s,a,snd t):trans_of B;fst s=fst t|]\
 \  ==> (s,a,t):trans_of (A||B)";
 by (asm_full_simp_tac (simpset() addsimps [Let_def,par_def,trans_of_def]) 1);
@@ -397,7 +396,7 @@
 qed "trans_of_par4";
 
 
-(* ---------------------------------------------------------------------------------- *)
+(* ------------------------------------------------------------------------- *)
 
 section "proof obligation generator for IOA requirements";  
 
@@ -407,12 +406,12 @@
 qed"is_trans_of_par";
 
 Goalw [is_trans_of_def] 
-"!!A. is_trans_of A ==> is_trans_of (restrict A acts)";
+"is_trans_of A ==> is_trans_of (restrict A acts)";
 by (asm_simp_tac (simpset() addsimps [cancel_restrict,acts_restrict])1);
 qed"is_trans_of_restrict";
 
 Goalw [is_trans_of_def,restrict_def,restrict_asig_def] 
-"!!A. is_trans_of A ==> is_trans_of (rename A f)";
+"is_trans_of A ==> is_trans_of (rename A f)";
 by (asm_full_simp_tac
     (simpset() addsimps [Let_def,actions_def,trans_of_def, asig_internals_def,
 			 asig_outputs_def,asig_inputs_def,externals_def,
@@ -420,31 +419,29 @@
 by (Blast_tac 1);
 qed"is_trans_of_rename";
 
-Goal "!! A. [| is_asig_of A; is_asig_of B; compatible A B|]  \
+Goal "[| is_asig_of A; is_asig_of B; compatible A B|]  \
 \         ==> is_asig_of (A||B)";
 by (asm_full_simp_tac (simpset() addsimps [is_asig_of_def,asig_of_par,
        asig_comp_def,compatible_def,asig_internals_def,asig_outputs_def,
      asig_inputs_def,actions_def,is_asig_def]) 1);
 by (asm_full_simp_tac (simpset() addsimps [asig_of_def]) 1);
 by Auto_tac;
-by (REPEAT (best_tac (set_cs addEs [equalityCE]) 1));
 qed"is_asig_of_par";
 
 Goalw [is_asig_of_def,is_asig_def,asig_of_def,restrict_def,restrict_asig_def,
            asig_internals_def,asig_outputs_def,asig_inputs_def,externals_def,o_def] 
-"!! A. is_asig_of A ==> is_asig_of (restrict A f)";
+"is_asig_of A ==> is_asig_of (restrict A f)";
 by (Asm_full_simp_tac 1);
 by Auto_tac;
-by (REPEAT (best_tac (set_cs addEs [equalityCE]) 1));
 qed"is_asig_of_restrict";
 
-Goal "!! A. is_asig_of A ==> is_asig_of (rename A f)";
+Goal "is_asig_of A ==> is_asig_of (rename A f)";
 by (asm_full_simp_tac (simpset() addsimps [is_asig_of_def,
      rename_def,rename_set_def,asig_internals_def,asig_outputs_def,
      asig_inputs_def,actions_def,is_asig_def,asig_of_def]) 1);
 by Auto_tac; 
 by   (ALLGOALS(dres_inst_tac [("s","Some ?x")] sym THEN' Asm_full_simp_tac));
-by   (ALLGOALS(best_tac (set_cs addEs [equalityCE])));
+by   (ALLGOALS(Blast_tac));
 qed"is_asig_of_rename";
 
 
@@ -453,28 +450,26 @@
 
 
 Goalw [compatible_def]
-"!! A. [|compatible A B; compatible A C |]==> compatible A (B||C)";
+"[|compatible A B; compatible A C |]==> compatible A (B||C)";
 by (asm_full_simp_tac (simpset() addsimps [internals_of_par, 
    outputs_of_par,actions_of_par]) 1);
 by Auto_tac;
-by (REPEAT (best_tac (set_cs addEs [equalityCE]) 1));
 qed"compatible_par";
 
 (*  better derive by previous one and compat_commute *)
 Goalw [compatible_def]
-"!! A. [|compatible A C; compatible B C |]==> compatible (A||B) C";
+"[|compatible A C; compatible B C |]==> compatible (A||B) C";
 by (asm_full_simp_tac (simpset() addsimps [internals_of_par, 
    outputs_of_par,actions_of_par]) 1);
 by Auto_tac;
-by (REPEAT (best_tac (set_cs addEs [equalityCE]) 1));
 qed"compatible_par2";
 
 Goalw [compatible_def]
-"!! A. [| compatible A B; (ext B - S) Int ext A = {}|] \
+"[| compatible A B; (ext B - S) Int ext A = {}|] \
 \     ==> compatible A (restrict B S)";
 by (asm_full_simp_tac (simpset() addsimps [ioa_triple_proj,asig_triple_proj,
           externals_def,restrict_def,restrict_asig_def,actions_def]) 1);
-by (auto_tac (claset() addEs [equalityCE],simpset()));
+by Auto_tac;
 qed"compatible_restrict";
 
 
diff -r 32c0b8f57bb7 -r bc2a76ce1ea3 src/HOLCF/IOA/meta_theory/CompoScheds.ML
--- a/src/HOLCF/IOA/meta_theory/CompoScheds.ML	Thu Jan 28 18:28:06 1999 +0100
+++ b/src/HOLCF/IOA/meta_theory/CompoScheds.ML	Fri Jan 29 16:23:56 1999 +0100
@@ -66,7 +66,7 @@
 by (Simp_tac 1);
 qed"mkex2_nil";
 
-Goal "!!x.[| x:act A; x~:act B; HD`exA=Def a|] \
+Goal "[| x:act A; x~:act B; HD`exA=Def a|] \
 \   ==> (mkex2 A B`(x>>sch)`exA`exB) s t =   \
 \       (x,snd a,t) >> (mkex2 A B`sch`(TL`exA)`exB) (snd a) t";
 by (rtac trans 1);
@@ -75,7 +75,7 @@
 by (asm_full_simp_tac (simpset() addsimps [Cons_def]) 1);
 qed"mkex2_cons_1";
 
-Goal "!!x.[| x~:act A; x:act B; HD`exB=Def b|] \
+Goal "[| x~:act A; x:act B; HD`exB=Def b|] \
 \   ==> (mkex2 A B`(x>>sch)`exA`exB) s t = \
 \       (x,s,snd b) >> (mkex2 A B`sch`exA`(TL`exB)) s (snd b)";
 by (rtac trans 1);
@@ -84,7 +84,7 @@
 by (asm_full_simp_tac (simpset() addsimps [Cons_def]) 1);
 qed"mkex2_cons_2";
 
-Goal "!!x.[| x:act A; x:act B; HD`exA=Def a;HD`exB=Def b|] \
+Goal "[| x:act A; x:act B; HD`exA=Def a;HD`exB=Def b|] \
 \   ==> (mkex2 A B`(x>>sch)`exA`exB) s t =  \
 \        (x,snd a,snd b) >> \
 \           (mkex2 A B`sch`(TL`exA)`(TL`exB)) (snd a) (snd b)";
@@ -109,7 +109,7 @@
 by (simp_tac (simpset() addsimps [mkex_def]) 1);
 qed"mkex_nil";
 
-Goal "!!x.[| x:act A; x~:act B |] \
+Goal "[| x:act A; x~:act B |] \
 \   ==> mkex A B (x>>sch) (s,a>>exA) (t,exB)  =  \
 \       ((s,t), (x,snd a,t) >> snd (mkex A B sch (snd a,exA) (t,exB)))";
 by (simp_tac (simpset() addsimps [mkex_def]) 1);
@@ -117,7 +117,7 @@
 by Auto_tac;
 qed"mkex_cons_1";
 
-Goal "!!x.[| x~:act A; x:act B |] \
+Goal "[| x~:act A; x:act B |] \
 \   ==> mkex A B (x>>sch) (s,exA) (t,b>>exB) =  \ 
 \       ((s,t), (x,s,snd b) >> snd (mkex A B sch (s,exA) (snd b,exB)))";
 by (simp_tac (simpset() addsimps [mkex_def]) 1);
@@ -125,7 +125,7 @@
 by Auto_tac;
 qed"mkex_cons_2";
 
-Goal "!!x.[| x:act A; x:act B |]  \
+Goal "[| x:act A; x:act B |]  \
 \   ==>  mkex A B (x>>sch) (s,a>>exA) (t,b>>exB) = \
 \        ((s,t), (x,snd a,snd b) >> snd (mkex A B sch (snd a,exA) (snd b,exB)))";
 by (simp_tac (simpset() addsimps [mkex_def]) 1);
@@ -277,7 +277,7 @@
 qed"stutterA_mkex";
 
 
-Goal "!! sch.[|  \
+Goal "[|  \
 \ Forall (%x. x:act (A||B)) sch ; \
 \ Filter (%a. a:act A)`sch << filter_act`(snd exA) ;\
 \ Filter (%a. a:act B)`sch << filter_act`(snd exB) |] \
@@ -308,7 +308,7 @@
 qed"stutterB_mkex";
 
 
-Goal "!! sch.[|  \
+Goal "[|  \
 \ Forall (%x. x:act (A||B)) sch ; \
 \ Filter (%a. a:act A)`sch << filter_act`(snd exA) ;\
 \ Filter (%a. a:act B)`sch << filter_act`(snd exB) |] \
diff -r 32c0b8f57bb7 -r bc2a76ce1ea3 src/HOLCF/IOA/meta_theory/CompoTraces.ML
--- a/src/HOLCF/IOA/meta_theory/CompoTraces.ML	Thu Jan 28 18:28:06 1999 +0100
+++ b/src/HOLCF/IOA/meta_theory/CompoTraces.ML	Fri Jan 29 16:23:56 1999 +0100
@@ -60,7 +60,7 @@
 by (Simp_tac 1);
 qed"mksch_nil";
 
-Goal "!!x.[|x:act A;x~:act B|]  \
+Goal "[|x:act A;x~:act B|]  \
 \   ==> mksch A B`(x>>tr)`schA`schB = \
 \         (Takewhile (%a. a:int A)`schA) \
 \         @@ (x>>(mksch A B`tr`(TL`(Dropwhile (%a. a:int A)`schA)) \
@@ -71,7 +71,7 @@
 by (simp_tac (simpset() addsimps [Cons_def]) 1);
 qed"mksch_cons1";
 
-Goal "!!x.[|x~:act A;x:act B|] \
+Goal "[|x~:act A;x:act B|] \
 \   ==> mksch A B`(x>>tr)`schA`schB = \
 \        (Takewhile (%a. a:int B)`schB)  \
 \         @@ (x>>(mksch A B`tr`schA`(TL`(Dropwhile (%a. a:int B)`schB))  \
@@ -82,7 +82,7 @@
 by (simp_tac (simpset() addsimps [Cons_def]) 1);
 qed"mksch_cons2";
 
-Goal "!!x.[|x:act A;x:act B|] \
+Goal "[|x:act A;x:act B|] \
 \   ==> mksch A B`(x>>tr)`schA`schB = \
 \            (Takewhile (%a. a:int A)`schA) \
 \         @@ ((Takewhile (%a. a:int B)`schB)  \
@@ -199,7 +199,7 @@
 (* safe-tac makes too many case distinctions with this lemma in the next proof *)
 Delsimps [FiniteConc];
 
-Goal "!! tr. [| Finite tr; is_asig(asig_of A); is_asig(asig_of B) |] ==> \
+Goal "[| Finite tr; is_asig(asig_of A); is_asig(asig_of B) |] ==> \
 \   ! x y. Forall (%x. x:act A) x & Forall (%x. x:act B) y & \
 \          Filter (%a. a:ext A)`x = Filter (%a. a:act A)`tr & \
 \          Filter (%a. a:ext B)`y = Filter (%a. a:act B)`tr &\
@@ -272,7 +272,7 @@
 (* otherwise subst_lemma2 does not fit exactly, just to avoid a subst_lemma3 *)
 Delsimps [FilterConc]; 
 
-Goal " !!bs. [| Finite bs; is_asig(asig_of A); is_asig(asig_of B);compatible A B|] ==>  \
+Goal " [| Finite bs; is_asig(asig_of A); is_asig(asig_of B);compatible A B|] ==>  \
 \! y. Forall (%x. x:act B) y & Forall (%x. x:act B & x~:act A) bs &\
 \    Filter (%a. a:ext B)`y = Filter (%a. a:act B)`(bs @@ z) \
 \    --> (? y1 y2.  (mksch A B`(bs @@ z)`x`y) = (y1 @@ (mksch A B`z`x`y2)) & \
@@ -326,7 +326,7 @@
 Delsimps [FilterConc]; 
 
 
-Goal " !!as. [| Finite as; is_asig(asig_of A); is_asig(asig_of B);compatible A B|] ==>  \
+Goal " [| Finite as; is_asig(asig_of A); is_asig(asig_of B);compatible A B|] ==>  \
 \! x. Forall (%x. x:act A) x & Forall (%x. x:act A & x~:act B) as &\
 \    Filter (%a. a:ext A)`x = Filter (%a. a:act A)`(as @@ z) \
 \    --> (? x1 x2.  (mksch A B`(as @@ z)`x`y) = (x1 @@ (mksch A B`z`x2`y)) & \
@@ -379,7 +379,7 @@
 (*
 
 
-Goal "!! y.Finite y ==> ! z tr. Forall (%a.a:ext (A||B)) tr & \
+Goal "Finite y ==> ! z tr. Forall (%a.a:ext (A||B)) tr & \
 \                             y = z @@ mksch A B`tr`a`b\
 \                             --> Finite tr";
 by (etac Seq_Finite_ind  1);
diff -r 32c0b8f57bb7 -r bc2a76ce1ea3 src/HOLCF/IOA/meta_theory/Compositionality.ML
--- a/src/HOLCF/IOA/meta_theory/Compositionality.ML	Thu Jan 28 18:28:06 1999 +0100
+++ b/src/HOLCF/IOA/meta_theory/Compositionality.ML	Fri Jan 29 16:23:56 1999 +0100
@@ -8,7 +8,7 @@
 
 
 
-Goal "!! A. [|eA --> A ; eB & ~eA --> ~A|] ==> (eA | eB) --> A=eA";
+Goal "[|eA --> A ; eB & ~eA --> ~A|] ==> (eA | eB) --> A=eA";
 by Auto_tac;
 qed"compatibility_consequence3";
 
@@ -27,12 +27,11 @@
 
 (* the next two theorems are only necessary, as there is no theorem ext (A||B) = ext (B||A) *)
 
-Goal "!! A. [|eA --> A ; eB & ~eA --> ~A|] ==> (eB | eA) --> A=eA";
+Goal "[|eA --> A ; eB & ~eA --> ~A|] ==> (eB | eA) --> A=eA";
 by Auto_tac;
 qed"compatibility_consequence4";
 
-Goal 
-"!! A B. [| compatible A B; Forall (%a. a: ext B | a: ext A) tr |] ==> \
+Goal "[| compatible A B; Forall (%a. a: ext B | a: ext A) tr |] ==> \
 \           Filter (%a. a: act A)`tr= Filter (%a. a: ext A)`tr";
 by (rtac ForallPFilterQR 1);
 by (assume_tac 2);
@@ -48,8 +47,7 @@
 
 
 
-Goal "!! A1 A2 B1 B2. \
-\         [| is_trans_of A1; is_trans_of A2; is_trans_of B1; is_trans_of B2;\
+Goal "[| is_trans_of A1; is_trans_of A2; is_trans_of B1; is_trans_of B2;\
 \            is_asig_of A1; is_asig_of A2; \
 \            is_asig_of B1; is_asig_of B2; \
 \            compatible A1 B1; compatible A2 B2; \
diff -r 32c0b8f57bb7 -r bc2a76ce1ea3 src/HOLCF/IOA/meta_theory/Deadlock.ML
--- a/src/HOLCF/IOA/meta_theory/Deadlock.ML	Thu Jan 28 18:28:06 1999 +0100
+++ b/src/HOLCF/IOA/meta_theory/Deadlock.ML	Fri Jan 29 16:23:56 1999 +0100
@@ -10,14 +10,14 @@
                input actions may always be added to a schedule
 **********************************************************************************)
 
-Goal "!! sch. [| Filter (%x. x:act A)`sch : schedules A; a:inp A; input_enabled A; Finite sch|] \
+Goal "[| Filter (%x. x:act A)`sch : schedules A; a:inp A; input_enabled A; Finite sch|] \
 \         ==> Filter (%x. x:act A)`sch @@ a>>nil : schedules A";
 by (asm_full_simp_tac (simpset() addsimps [schedules_def,has_schedule_def]) 1);
 by (safe_tac set_cs);
 by (forward_tac  [inp_is_act] 1);
 by (asm_full_simp_tac (simpset() addsimps [executions_def]) 1);
 by (pair_tac "ex" 1);
-ren "sch s ex" 1;
+ren "s ex" 1;
 by (subgoal_tac "Finite ex" 1);
 by (asm_full_simp_tac (simpset() addsimps [filter_act_def]) 2);
 by (rtac (Map2Finite RS iffD1) 2);
@@ -51,7 +51,7 @@
                     and distributivity of is_exec_frag over @@
 **********************************************************************************)
 Delsplits [split_if];
-Goal "!! sch. [| a : local A; Finite sch; sch : schedules (A||B); \
+Goal "[| a : local A; Finite sch; sch : schedules (A||B); \
 \            Filter (%x. x:act A)`(sch @@ a>>nil) : schedules A; compatible A B; input_enabled B |] \
 \          ==> (sch @@ a>>nil) : schedules (A||B)";
 
diff -r 32c0b8f57bb7 -r bc2a76ce1ea3 src/HOLCF/IOA/meta_theory/LiveIOA.ML
--- a/src/HOLCF/IOA/meta_theory/LiveIOA.ML	Thu Jan 28 18:28:06 1999 +0100
+++ b/src/HOLCF/IOA/meta_theory/LiveIOA.ML	Fri Jan 29 16:23:56 1999 +0100
@@ -10,7 +10,7 @@
 Delsimps [split_paired_Ex];
 
 Goalw [live_implements_def] 
-"!! A. [| live_implements (A,LA) (B,LB); live_implements (B,LB) (C,LC) |] \
+"[| live_implements (A,LA) (B,LB); live_implements (B,LB) (C,LC) |] \
 \     ==> live_implements (A,LA) (C,LC)"; 
 by Auto_tac;
 qed"live_implements_trans";
@@ -24,7 +24,7 @@
 (* ---------------------------------------------------------------- *)
 
 
-Goal "!! f. [| inp(C)=inp(A); out(C)=out(A); \
+Goal "[| inp(C)=inp(A); out(C)=out(A); \
 \                  is_live_ref_map f (C,M) (A,L) |] \
 \               ==> live_implements (C,M) (A,L)";
 
diff -r 32c0b8f57bb7 -r bc2a76ce1ea3 src/HOLCF/IOA/meta_theory/RefCorrectness.ML
--- a/src/HOLCF/IOA/meta_theory/RefCorrectness.ML	Thu Jan 28 18:28:06 1999 +0100
+++ b/src/HOLCF/IOA/meta_theory/RefCorrectness.ML	Fri Jan 29 16:23:56 1999 +0100
@@ -62,7 +62,7 @@
 section"properties of move";
 
 Goalw [is_ref_map_def]
-   "!!f. [|is_ref_map f C A; reachable C s; (s,a,t):trans_of C|] ==>\
+   "[|is_ref_map f C A; reachable C s; (s,a,t):trans_of C|] ==>\
 \     move A (@x. move A x (f s) a (f t)) (f s) a (f t)";
 
 by (subgoal_tac "? ex. move A ex (f s) a (f t)" 1);
@@ -73,7 +73,7 @@
 qed"move_is_move";
 
 Goal
-   "!!f. [|is_ref_map f C A; reachable C s; (s,a,t):trans_of C|] ==>\
+   "[|is_ref_map f C A; reachable C s; (s,a,t):trans_of C|] ==>\
 \    is_exec_frag A (f s,@x. move A x (f s) a (f t))";
 by (cut_inst_tac [] move_is_move 1);
 by (REPEAT (assume_tac 1));
@@ -81,7 +81,7 @@
 qed"move_subprop1";
 
 Goal
-   "!!f. [|is_ref_map f C A; reachable C s; (s,a,t):trans_of C|] ==>\
+   "[|is_ref_map f C A; reachable C s; (s,a,t):trans_of C|] ==>\
 \    Finite ((@x. move A x (f s) a (f t)))";
 by (cut_inst_tac [] move_is_move 1);
 by (REPEAT (assume_tac 1));
@@ -89,7 +89,7 @@
 qed"move_subprop2";
 
 Goal
-   "!!f. [|is_ref_map f C A; reachable C s; (s,a,t):trans_of C|] ==>\
+   "[|is_ref_map f C A; reachable C s; (s,a,t):trans_of C|] ==>\
 \    laststate (f s,@x. move A x (f s) a (f t)) = (f t)";
 by (cut_inst_tac [] move_is_move 1);
 by (REPEAT (assume_tac 1));
@@ -97,7 +97,7 @@
 qed"move_subprop3";
 
 Goal
-   "!!f. [|is_ref_map f C A; reachable C s; (s,a,t):trans_of C|] ==>\
+   "[|is_ref_map f C A; reachable C s; (s,a,t):trans_of C|] ==>\
 \     mk_trace A`((@x. move A x (f s) a (f t))) = \
 \       (if a:ext A then a>>nil else nil)";
 
@@ -131,7 +131,7 @@
    ------------------------------------------------------- *)
 Delsplits[split_if];
 Goalw [corresp_ex_def]
-  "!!f.[|is_ref_map f C A; ext C = ext A|] ==>  \     
+  "[|is_ref_map f C A; ext C = ext A|] ==>  \     
 \        !s. reachable C s & is_exec_frag C (s,xs) --> \
 \            mk_trace C`xs = mk_trace A`(snd (corresp_ex A f (s,xs)))";
 
@@ -180,7 +180,7 @@
 
 
 Goalw [corresp_ex_def]
- "!!f.[| is_ref_map f C A |] ==>\
+ "[| is_ref_map f C A |] ==>\
 \ !s. reachable C s & is_exec_frag C (s,xs) \
 \ --> is_exec_frag A (corresp_ex A f (s,xs))"; 
 
@@ -221,7 +221,7 @@
 
 
 Goalw [traces_def]
-  "!!f. [| ext C = ext A; is_ref_map f C A |] \
+  "[| ext C = ext A; is_ref_map f C A |] \
 \          ==> traces C <= traces A"; 
 
   by (simp_tac(simpset() addsimps [has_trace_def2])1);
@@ -260,15 +260,13 @@
 qed"fininf";
 
 
-Goal 
-"is_wfair A W (s,ex) = \
+Goal "is_wfair A W (s,ex) = \
 \ (fin_often (%x. ~Enabled A W (snd x)) ex --> inf_often (%x. fst x :W) ex)";
 by (asm_full_simp_tac (simpset() addsimps [is_wfair_def,fin_often_def])1);
 by Auto_tac;
 qed"WF_alt";
 
-Goal  
-"!! ex. [|is_wfair A W (s,ex); inf_often (%x. Enabled A W (snd x)) ex; \
+Goal "[|is_wfair A W (s,ex); inf_often (%x. Enabled A W (snd x)) ex; \
 \         en_persistent A W|] \
 \   ==> inf_often (%x. fst x :W) ex";
 by (dtac persistent 1);
diff -r 32c0b8f57bb7 -r bc2a76ce1ea3 src/HOLCF/IOA/meta_theory/RefMappings.ML
--- a/src/HOLCF/IOA/meta_theory/RefMappings.ML	Thu Jan 28 18:28:06 1999 +0100
+++ b/src/HOLCF/IOA/meta_theory/RefMappings.ML	Fri Jan 29 16:23:56 1999 +0100
@@ -15,21 +15,21 @@
 section "transitions and moves";
 
 
-Goal"!!f. s -a--A-> t ==> ? ex. move A ex s a t";
+Goal "s -a--A-> t ==> ? ex. move A ex s a t";
 
 by (res_inst_tac [("x","(a,t)>>nil")] exI 1);
 by (asm_full_simp_tac (simpset() addsimps [move_def]) 1);
 qed"transition_is_ex";
  
 
-Goal"!!f. (~a:ext A) & s=t ==> ? ex. move A ex s a t";
+Goal "(~a:ext A) & s=t ==> ? ex. move A ex s a t";
 
 by (res_inst_tac [("x","nil")] exI 1);
 by (asm_full_simp_tac (simpset() addsimps [move_def]) 1);
 qed"nothing_is_ex";
 
 
-Goal"!!f. (s -a--A-> s') & (s' -a'--A-> s'') & (~a':ext A) \
+Goal "(s -a--A-> s') & (s' -a'--A-> s'') & (~a':ext A) \
 \        ==> ? ex. move A ex s a s''";
 
 by (res_inst_tac [("x","(a,s')>>(a',s'')>>nil")] exI 1);
@@ -37,8 +37,7 @@
 qed"ei_transitions_are_ex";
 
 
-Goal
-"!!f. (s1 -a1--A-> s2) & (s2 -a2--A-> s3) & (s3 -a3--A-> s4) &\
+Goal "(s1 -a1--A-> s2) & (s2 -a2--A-> s3) & (s3 -a3--A-> s4) &\
 \     (~a2:ext A) & (~a3:ext A) ==> \
 \     ? ex. move A ex s1 a1 s4";
   
@@ -53,7 +52,7 @@
 
 
 Goalw [is_weak_ref_map_def,is_ref_map_def]
-  "!!f. [| ext C = ext A; \
+  "[| ext C = ext A; \
 \    is_weak_ref_map f C A |] ==> is_ref_map f C A";
 by (safe_tac set_cs);
 by (case_tac "a:ext A" 1);
@@ -69,7 +68,7 @@
 val lemma = result();
 
 Delsplits [split_if];
-Goal "!!f.[| is_weak_ref_map f C A |]\
+Goal "[| is_weak_ref_map f C A |]\
 \                      ==> (is_weak_ref_map f (rename C g) (rename A g))";
 by (asm_full_simp_tac (simpset() addsimps [is_weak_ref_map_def]) 1);
 by (rtac conjI 1);
diff -r 32c0b8f57bb7 -r bc2a76ce1ea3 src/HOLCF/IOA/meta_theory/Seq.ML
--- a/src/HOLCF/IOA/meta_theory/Seq.ML	Thu Jan 28 18:28:06 1999 +0100
+++ b/src/HOLCF/IOA/meta_theory/Seq.ML	Fri Jan 29 16:23:56 1999 +0100
@@ -47,7 +47,7 @@
 qed"smap_UU";
 
 Goal 
-"!!x.[|x~=UU|] ==> smap`f`(x##xs)= (f`x)##smap`f`xs"; 
+"[|x~=UU|] ==> smap`f`(x##xs)= (f`x)##smap`f`xs"; 
 by (rtac trans 1);
 by (stac smap_unfold 1);
 by (Asm_full_simp_tac 1);
@@ -74,7 +74,7 @@
 qed"sfilter_UU";
 
 Goal 
-"!!x. x~=UU ==> sfilter`P`(x##xs)=   \
+"x~=UU ==> sfilter`P`(x##xs)=   \
 \             (If P`x then x##(sfilter`P`xs) else sfilter`P`xs fi)";
 by (rtac trans 1);
 by (stac sfilter_unfold 1);
@@ -102,7 +102,7 @@
 qed"sforall2_UU";
 
 Goal 
-"!!x. x~=UU ==> sforall2`P`(x##xs)= ((P`x) andalso sforall2`P`xs)";
+"x~=UU ==> sforall2`P`(x##xs)= ((P`x) andalso sforall2`P`xs)";
 by (rtac trans 1);
 by (stac sforall2_unfold 1);
 by (Asm_full_simp_tac 1);
@@ -131,7 +131,7 @@
 qed"stakewhile_UU";
 
 Goal 
-"!!x. x~=UU ==> stakewhile`P`(x##xs) =   \
+"x~=UU ==> stakewhile`P`(x##xs) =   \
 \             (If P`x then x##(stakewhile`P`xs) else nil fi)";
 by (rtac trans 1);
 by (stac stakewhile_unfold 1);
@@ -160,7 +160,7 @@
 qed"sdropwhile_UU";
 
 Goal 
-"!!x. x~=UU ==> sdropwhile`P`(x##xs) =   \
+"x~=UU ==> sdropwhile`P`(x##xs) =   \
 \             (If P`x then sdropwhile`P`xs else x##xs fi)";
 by (rtac trans 1);
 by (stac sdropwhile_unfold 1);
@@ -191,7 +191,7 @@
 qed"slast_UU";
 
 Goal 
-"!!x. x~=UU ==> slast`(x##xs)= (If is_nil`xs then x else slast`xs fi)";
+"x~=UU ==> slast`(x##xs)= (If is_nil`xs then x else slast`xs fi)";
 by (rtac trans 1);
 by (stac slast_unfold 1);
 by (Asm_full_simp_tac 1);
@@ -281,20 +281,20 @@
 by (Simp_tac 1);
 qed"szip_UU1";
 
-Goal "!!x. x~=nil ==> szip`x`UU=UU"; 
+Goal "x~=nil ==> szip`x`UU=UU"; 
 by (stac szip_unfold 1);
 by (Asm_full_simp_tac 1);
 by (res_inst_tac [("x","x")] seq.casedist 1);
 by (REPEAT (Asm_full_simp_tac 1));
 qed"szip_UU2";
 
-Goal "!!x. x~=UU ==> szip`(x##xs)`nil=UU";
+Goal "x~=UU ==> szip`(x##xs)`nil=UU";
 by (rtac trans 1);
 by (stac szip_unfold 1);
 by (REPEAT (Asm_full_simp_tac 1));
 qed"szip_cons_nil";
 
-Goal "!!x.[| x~=UU; y~=UU|] ==> szip`(x##xs)`(y##ys) = <x,y>##szip`xs`ys";
+Goal "[| x~=UU; y~=UU|] ==> szip`(x##xs)`(y##ys) = <x,y>##szip`xs`ys";
 by (rtac trans 1);
 by (stac szip_unfold 1);
 by (REPEAT (Asm_full_simp_tac 1));
@@ -317,13 +317,13 @@
 section "scons, nil";
 
 Goal 
- "!!x. [|x~=UU;y~=UU|]==> (x##xs=y##ys) = (x=y & xs=ys)";
+ "[|x~=UU;y~=UU|]==> (x##xs=y##ys) = (x=y & xs=ys)";
 by (rtac iffI 1);
 by (etac (hd seq.injects) 1);
 by Auto_tac;
 qed"scons_inject_eq";
 
-Goal "!!x. nil<<x ==> nil=x";
+Goal "nil<<x ==> nil=x";
 by (res_inst_tac [("x","x")] seq.casedist 1);
 by (hyp_subst_tac 1);
 by (etac antisym_less 1);
@@ -416,7 +416,7 @@
 by (fast_tac (HOL_cs addSDs seq.injects) 1);
 qed"Finite_cons_a";
 
-Goal "!!x. a~=UU ==>(Finite (a##x)) = (Finite x)";
+Goal "a~=UU ==>(Finite (a##x)) = (Finite x)";
 by (rtac iffI 1);
 by (rtac (Finite_cons_a RS mp RS mp RS mp) 1);
 by (REPEAT (assume_tac 1));
@@ -448,8 +448,7 @@
         ]);
 
 
-Goal 
-"!!P.[|P(UU);P(nil);\
+Goal "!!P.[|P(UU);P(nil);\
 \  !! x s1.[|x~=UU;P(s1)|] ==> P(x##s1)\
 \  |] ==> seq_finite(s) --> P(s)";
 by (rtac seq_finite_ind_lemma 1);
diff -r 32c0b8f57bb7 -r bc2a76ce1ea3 src/HOLCF/IOA/meta_theory/Sequence.ML
--- a/src/HOLCF/IOA/meta_theory/Sequence.ML	Thu Jan 28 18:28:06 1999 +0100
+++ b/src/HOLCF/IOA/meta_theory/Sequence.ML	Fri Jan 29 16:23:56 1999 +0100
@@ -167,7 +167,7 @@
 by (Simp_tac 1);
 qed"Zip_UU1";
 
-Goal "!! x. x~=nil ==> Zip`x`UU =UU";
+Goal "x~=nil ==> Zip`x`UU =UU";
 by (stac Zip_unfold 1);
 by (Simp_tac 1);
 by (res_inst_tac [("x","x")] seq.casedist 1);
@@ -384,11 +384,11 @@
 qed"Finite_Cons";
 
 Addsimps [Finite_Cons];
-Goal "!! x. Finite (x::'a Seq) ==> Finite y --> Finite (x@@y)";
+Goal "Finite (x::'a Seq) ==> Finite y --> Finite (x@@y)";
 by (Seq_Finite_induct_tac 1);
 qed"FiniteConc_1";
 
-Goal "!! z. Finite (z::'a Seq) ==> !x y. z= x@@y --> (Finite x & Finite y)";
+Goal "Finite (z::'a Seq) ==> !x y. z= x@@y --> (Finite x & Finite y)";
 by (Seq_Finite_induct_tac 1);
 (* nil*)
 by (strip_tac 1);
@@ -415,11 +415,11 @@
 Addsimps [FiniteConc];
 
 
-Goal "!! s. Finite s ==> Finite (Map f`s)";
+Goal "Finite s ==> Finite (Map f`s)";
 by (Seq_Finite_induct_tac 1);
 qed"FiniteMap1";
 
-Goal "!! s. Finite s ==> ! t. (s = Map f`t) --> Finite t";
+Goal "Finite s ==> ! t. (s = Map f`t) --> Finite t";
 by (Seq_Finite_induct_tac 1);
 by (strip_tac 1);
 by (Seq_case_simp_tac "t" 1);
@@ -438,7 +438,7 @@
 qed"Map2Finite";
 
 
-Goal "!! s. Finite s ==> Finite (Filter P`s)";
+Goal "Finite s ==> Finite (Filter P`s)";
 by (Seq_Finite_induct_tac 1);
 qed"FiniteFilter";
 
@@ -519,11 +519,11 @@
 
 section "Last";
 
-Goal "!! s. Finite s ==> s~=nil --> Last`s~=UU";
+Goal "Finite s ==> s~=nil --> Last`s~=UU";
 by (Seq_Finite_induct_tac  1);
 qed"Finite_Last1";
 
-Goal "!! s. Finite s ==> Last`s=UU --> s=nil";
+Goal "Finite s ==> Last`s=UU --> s=nil";
 by (Seq_Finite_induct_tac  1);
 by (fast_tac HOL_cs 1);
 qed"Finite_Last2";
@@ -587,7 +587,7 @@
 by (Seq_induct_tac "x" [Forall_def,sforall_def] 1);
 qed"Forall_Conc_impl";
 
-Goal "!! x. Finite x ==> Forall P (x @@ y) = (Forall P x & Forall P y)";
+Goal "Finite x ==> Forall P (x @@ y) = (Forall P x & Forall P y)";
 by (Seq_Finite_induct_tac  1);
 qed"Forall_Conc";
 
@@ -619,7 +619,7 @@
 bind_thm ("Forall_prefixclosed",Forall_prefix RS spec RS mp RS mp);
 
 
-Goal "!! h. [| Finite h; Forall P s; s= h @@ t |] ==> Forall P t";
+Goal "[| Finite h; Forall P s; s= h @@ t |] ==> Forall P t";
 by Auto_tac;
 qed"Forall_postfixclosed";
 
@@ -658,7 +658,7 @@
 
 
 (* holds also in other direction *)
-Goal   "!! P. ~Finite ys & Forall (%x. ~P x) ys \
+Goal   "~Finite ys & Forall (%x. ~P x) ys \
 \                  --> Filter P`ys = UU ";
 by (Seq_induct_tac "ys" [Forall_def,sforall_def] 1);
 qed"ForallnPFilterPUU1";
@@ -685,7 +685,7 @@
 
 (* inverse of ForallnPFilterPUU. proved by 2 lemmas because of adm problems *)
 
-Goal "!! ys. Finite ys ==> Filter P`ys ~= UU";
+Goal "Finite ys ==> Filter P`ys ~= UU";
 by (Seq_Finite_induct_tac 1);
 qed"FilterUU_nFinite_lemma1";
 
@@ -693,7 +693,7 @@
 by (Seq_induct_tac "ys" [Forall_def,sforall_def] 1);
 qed"FilterUU_nFinite_lemma2";
 
-Goal   "!! P. Filter P`ys = UU ==> \
+Goal   "Filter P`ys = UU ==> \
 \                (Forall (%x. ~P x) ys  & ~Finite ys)";
 by (rtac conjI 1);
 by (cut_inst_tac [] (FilterUU_nFinite_lemma2 RS mp COMP rev_contrapos) 1);
@@ -775,7 +775,7 @@
 
 bind_thm("TakewhileConc",TakewhileConc1 RS mp);
 
-Goal "!! s. Finite s ==> Forall P s --> Dropwhile P`(s @@ t) = Dropwhile P`t";
+Goal "Finite s ==> Forall P s --> Dropwhile P`(s @@ t) = Dropwhile P`t";
 by (Seq_Finite_induct_tac 1);
 qed"DropwhileConc1";
 
@@ -804,7 +804,7 @@
 by (Asm_full_simp_tac 1); 
 qed"divide_Seq_lemma";
 
-Goal "!! x. (x>>xs) << Filter P`y  \
+Goal "(x>>xs) << Filter P`y  \
 \   ==> y = ((Takewhile (%a. ~ P a)`y) @@ (x >> TL`(Dropwhile (%a.~P a)`y))) \
 \      & Finite (Takewhile (%a. ~ P a)`y)  & P x";
 by (rtac (divide_Seq_lemma RS mp) 1);
@@ -820,7 +820,7 @@
 qed"nForall_HDFilter";
 
 
-Goal "!!y. ~Forall P y  \
+Goal "~Forall P y  \
 \  ==> ? x. y= (Takewhile P`y @@ (x >> TL`(Dropwhile P`y))) & \
 \      Finite (Takewhile P`y) & (~ P x)";
 by (dtac (nForall_HDFilter RS mp) 1);
@@ -831,7 +831,7 @@
 qed"divide_Seq2";
 
 
-Goal  "!! y. ~Forall P y \
+Goal  "~Forall P y \
 \  ==> ? x bs rs. y= (bs @@ (x>>rs)) & Finite bs & Forall P bs & (~ P x)";
 by (cut_inst_tac [] divide_Seq2 1);
 (*Auto_tac no longer proves it*)
@@ -864,7 +864,7 @@
 qed"take_reduction1";
 
 
-Goal "!! n.[| x=y; s=t;!! k. k<n ==> seq_take k`y1 = seq_take k`y2|] \
+Goal "!! n.[| x=y; s=t; !! k. k<n ==> seq_take k`y1 = seq_take k`y2|] \
 \ ==> seq_take n`(x @@ (s>>y1)) =  seq_take n`(y @@ (t>>y2))";
 
 by (auto_tac (claset() addSIs [take_reduction1 RS spec RS mp],simpset()));
@@ -1117,13 +1117,13 @@
 by (Seq_induct_tac "s" [Forall_def,sforall_def] 1);
 qed"Filter_lemma1";
 
-Goal "!! s. Finite s ==>  \
+Goal "Finite s ==>  \
 \         (Forall (%x. (~P x) | (~ Q x)) s  \
 \         --> Filter P`(Filter Q`s) = nil)";
 by (Seq_Finite_induct_tac 1);
 qed"Filter_lemma2";
 
-Goal "!! s. Finite s ==>  \
+Goal "Finite s ==>  \
 \         Forall (%x. (~P x) | (~ Q x)) s  \
 \         --> Filter (%x. P x & Q x)`s = nil";
 by (Seq_Finite_induct_tac 1);
diff -r 32c0b8f57bb7 -r bc2a76ce1ea3 src/HOLCF/IOA/meta_theory/ShortExecutions.ML
--- a/src/HOLCF/IOA/meta_theory/ShortExecutions.ML	Thu Jan 28 18:28:06 1999 +0100
+++ b/src/HOLCF/IOA/meta_theory/ShortExecutions.ML	Fri Jan 29 16:23:56 1999 +0100
@@ -61,7 +61,7 @@
 (* ---------------------------------------------------------------- *)
 
 Goalw [Cut_def]
-"!! s. [| Forall (%a.~ P a) s; Finite s|] \
+"[| Forall (%a.~ P a) s; Finite s|] \
 \           ==> Cut P s =nil";
 by (subgoal_tac "Filter P`s = nil" 1);
 by (asm_simp_tac (simpset() addsimps [oraclebuild_nil]) 1);
@@ -70,7 +70,7 @@
 qed"Cut_nil";
 
 Goalw [Cut_def]
-"!! s. [| Forall (%a.~ P a) s; ~Finite s|] \
+"[| Forall (%a.~ P a) s; ~Finite s|] \
 \           ==> Cut P s =UU";
 by (subgoal_tac "Filter P`s= UU" 1);
 by (asm_simp_tac (simpset() addsimps [oraclebuild_UU]) 1);
@@ -79,7 +79,7 @@
 qed"Cut_UU";
 
 Goalw [Cut_def]
-"!! s. [| P t;  Forall (%x.~ P x) ss; Finite ss|] \
+"[| P t;  Forall (%x.~ P x) ss; Finite ss|] \
 \           ==> Cut P (ss @@ (t>> rs)) \
 \                = ss @@ (t >> Cut P rs)";
 
@@ -200,7 +200,7 @@
 
 
 Goalw [schedules_def,has_schedule_def]
- "!! sch. [|sch : schedules A ; tr = Filter (%a. a:ext A)`sch|] \
+ "[|sch : schedules A ; tr = Filter (%a. a:ext A)`sch|] \
 \   ==> ? sch. sch : schedules A & \
 \              tr = Filter (%a. a:ext A)`sch &\
 \              LastActExtsch A sch";
@@ -239,7 +239,7 @@
 (* ---------------------------------------------------------------- *)
 
 Goalw [LastActExtsch_def]
-  "!! A. [| LastActExtsch A sch; Filter (%x. x:ext A)`sch = nil |] \
+  "[| LastActExtsch A sch; Filter (%x. x:ext A)`sch = nil |] \
 \   ==> sch=nil";
 by (dtac FilternPnilForallP 1);
 by (etac conjE 1);
@@ -249,7 +249,7 @@
 qed"LastActExtimplnil";
 
 Goalw [LastActExtsch_def]
-  "!! A. [| LastActExtsch A sch; Filter (%x. x:ext A)`sch = UU |] \
+  "[| LastActExtsch A sch; Filter (%x. x:ext A)`sch = UU |] \
 \   ==> sch=UU";
 by (dtac FilternPUUForallP 1);
 by (etac conjE 1);
diff -r 32c0b8f57bb7 -r bc2a76ce1ea3 src/HOLCF/IOA/meta_theory/SimCorrectness.ML
--- a/src/HOLCF/IOA/meta_theory/SimCorrectness.ML	Thu Jan 28 18:28:06 1999 +0100
+++ b/src/HOLCF/IOA/meta_theory/SimCorrectness.ML	Fri Jan 29 16:23:56 1999 +0100
@@ -69,7 +69,7 @@
 Delsimps [Let_def];
 
 Goalw [is_simulation_def]
-   "!!f. [|is_simulation R C A; reachable C s; s -a--C-> t; (s,s'):R|] ==>\
+   "[|is_simulation R C A; reachable C s; s -a--C-> t; (s,s'):R|] ==>\
 \     let T' = @t'. ? ex1. (t,t'):R & move A ex1 s' a t' in \
 \     (t,T'): R & move A (@ex2. move A ex2 s' a T') s' a T'";
 
@@ -99,7 +99,7 @@
 Addsimps [Let_def];
 
 Goal
-   "!!f. [|is_simulation R C A; reachable C s; s-a--C-> t; (s,s'):R|] ==>\
+   "[|is_simulation R C A; reachable C s; s-a--C-> t; (s,s'):R|] ==>\
 \   let T' = @t'. ? ex1. (t,t'):R & move A ex1 s' a t' in \
 \    is_exec_frag A (s',@x. move A x s' a T')";
 by (cut_inst_tac [] move_is_move_sim 1);
@@ -108,7 +108,7 @@
 qed"move_subprop1_sim";
 
 Goal
-   "!!f. [|is_simulation R C A; reachable C s; s-a--C-> t; (s,s'):R|] ==>\
+   "[|is_simulation R C A; reachable C s; s-a--C-> t; (s,s'):R|] ==>\
 \   let T' = @t'. ? ex1. (t,t'):R & move A ex1 s' a t' in \
 \   Finite (@x. move A x s' a T')";
 by (cut_inst_tac [] move_is_move_sim 1);
@@ -117,7 +117,7 @@
 qed"move_subprop2_sim";
 
 Goal
-   "!!f. [|is_simulation R C A; reachable C s; s-a--C-> t; (s,s'):R|] ==>\
+   "[|is_simulation R C A; reachable C s; s-a--C-> t; (s,s'):R|] ==>\
 \   let T' = @t'. ? ex1. (t,t'):R & move A ex1 s' a t' in \
 \    laststate (s',@x. move A x s' a T') = T'";
 by (cut_inst_tac [] move_is_move_sim 1);
@@ -126,7 +126,7 @@
 qed"move_subprop3_sim";
 
 Goal
-   "!!f. [|is_simulation R C A; reachable C s; s-a--C-> t; (s,s'):R|] ==>\
+   "[|is_simulation R C A; reachable C s; s-a--C-> t; (s,s'):R|] ==>\
 \   let T' = @t'. ? ex1. (t,t'):R & move A ex1 s' a t' in \
 \     mk_trace A`((@x. move A x s' a T')) = \
 \       (if a:ext A then a>>nil else nil)";
@@ -136,7 +136,7 @@
 qed"move_subprop4_sim";
 
 Goal
-   "!!f. [|is_simulation R C A; reachable C s; s-a--C-> t; (s,s'):R|] ==>\
+   "[|is_simulation R C A; reachable C s; s-a--C-> t; (s,s'):R|] ==>\
 \   let T' = @t'. ? ex1. (t,t'):R & move A ex1 s' a t' in \
 \     (t,T'):R";
 by (cut_inst_tac [] move_is_move_sim 1);
@@ -158,7 +158,7 @@
 
 Delsplits[split_if];
 Goal 
-  "!!f.[|is_simulation R C A; ext C = ext A|] ==>  \     
+  "[|is_simulation R C A; ext C = ext A|] ==>  \     
 \        !s s'. reachable C s & is_exec_frag C (s,ex) & (s,s'): R --> \
 \            mk_trace C`ex = mk_trace A`((corresp_ex_simC A R`ex) s')";
 
@@ -188,7 +188,7 @@
 
 
 Goal 
- "!!f.[| is_simulation R C A |] ==>\
+ "[| is_simulation R C A |] ==>\
 \ !s s'. reachable C s & is_exec_frag C (s,ex) & (s,s'):R  \
 \ --> is_exec_frag A (s',(corresp_ex_simC A R`ex) s')"; 
 
@@ -240,7 +240,7 @@
      S':= @s'. (s,s'):R & s':starts_of A, where s:starts_of C  *)
 
 Goal 
-"!!C. [| is_simulation R C A; s:starts_of C |] \
+"[| is_simulation R C A; s:starts_of C |] \
 \ ==> let S' = @s'. (s,s'):R & s':starts_of A in \
 \     (s,S'):R & S':starts_of A";
   by (asm_full_simp_tac (simpset() addsimps [is_simulation_def,
@@ -259,7 +259,7 @@
 
 
 Goalw [traces_def]
-  "!!f. [| ext C = ext A; is_simulation R C A |] \
+  "[| ext C = ext A; is_simulation R C A |] \
 \          ==> traces C <= traces A"; 
 
   by (simp_tac(simpset() addsimps [has_trace_def2])1);
diff -r 32c0b8f57bb7 -r bc2a76ce1ea3 src/HOLCF/IOA/meta_theory/TL.ML
--- a/src/HOLCF/IOA/meta_theory/TL.ML	Thu Jan 28 18:28:06 1999 +0100
+++ b/src/HOLCF/IOA/meta_theory/TL.ML	Fri Jan 29 16:23:56 1999 +0100
@@ -50,7 +50,7 @@
 qed"reflT";
 
 
-Goal "!!x. [| suffix y x ; suffix z y |]  ==> suffix z x";
+Goal "[| suffix y x ; suffix z y |]  ==> suffix z x";
 by (asm_full_simp_tac (simpset() addsimps [suffix_def])1);
 by Auto_tac;
 by (res_inst_tac [("x","s1 @@ s1a")] exI 1);
@@ -79,21 +79,21 @@
 (*                      TLA Rules by Lamport                        *)
 (* ---------------------------------------------------------------- *)
 
-Goal "!! P. validT P ==> validT ([] P)";
+Goal "validT P ==> validT ([] P)";
 by (asm_full_simp_tac (simpset() addsimps [validT_def,satisfies_def,Box_def,tsuffix_def])1);
 qed"STL1a";
 
-Goal "!! P. valid P ==> validT (Init P)";
+Goal "valid P ==> validT (Init P)";
 by (asm_full_simp_tac (simpset() addsimps [valid_def,validT_def,satisfies_def,Init_def])1);
 qed"STL1b";
 
-Goal "!! P. valid P ==> validT ([] (Init P))";
+Goal "valid P ==> validT ([] (Init P))";
 by (rtac STL1a 1);
 by (etac STL1b 1);
 qed"STL1";
 
 (* Note that unlift and HD is not at all used !!! *)
-Goal "!! P. valid (P .--> Q)  ==> validT ([] (Init P) .--> [] (Init Q))";
+Goal "valid (P .--> Q)  ==> validT ([] (Init P) .--> [] (Init Q))";
 by (asm_full_simp_tac (simpset() addsimps [valid_def,validT_def,satisfies_def,IMPLIES_def,Box_def,Init_def])1);
 qed"STL4";
 
@@ -158,11 +158,11 @@
 
 
 
-Goal "!! P. [| validT (P .--> Q); validT P |] ==> validT Q";
+Goal "[| validT (P .--> Q); validT P |] ==> validT Q";
 by (asm_full_simp_tac (simpset() addsimps [validT_def,satisfies_def,IMPLIES_def])1);
 qed"ModusPonens";
 
 (* works only if validT is defined without restriction to s~=UU, s~=nil *)
-Goal "!! P. validT P ==> validT (Next P)";
+Goal "validT P ==> validT (Next P)";
 by (asm_full_simp_tac (simpset() addsimps [validT_def,satisfies_def,Next_def])1);
 (* qed"NextTauto"; *)
diff -r 32c0b8f57bb7 -r bc2a76ce1ea3 src/HOLCF/IOA/meta_theory/TLS.ML
--- 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);