src/HOLCF/IOA/NTP/Impl.ML

 goal Impl.thy
   "fst(x) = sen(x)            & \
 \  fst(snd(x)) = rec(x)       & \
 \  fst(snd(snd(x))) = srch(x) & \
 \  snd(snd(snd(x))) = rsch(x)";
-by(simp_tac (simpset() addsimps
+by (simp_tac (simpset() addsimps
              [sen_def,rec_def,srch_def,rsch_def]) 1);
 Addsimps [result()];
 
 goal Impl.thy "a:actions(sender_asig)   \
 \            | a:actions(receiver_asig) \
 \            | a:actions(srch_asig)     \
 \            | a:actions(rsch_asig)";
-  by(Action.action.induct_tac "a" 1);
-  by(ALLGOALS (Simp_tac));
+  by (Action.action.induct_tac "a" 1);
+  by (ALLGOALS (Simp_tac));
 Addsimps [result()];
 
 Delsimps [split_paired_All];
 
 

 
 (* INVARIANT 1 *)
 
 goalw Impl.thy impl_ioas "invariant impl_ioa inv1";
 by (rtac invariantI 1);
-by(asm_full_simp_tac (simpset()
+by (asm_full_simp_tac (simpset()
    addsimps [inv1_def, hdr_sum_def, Sender.srcvd_def,
              Sender.ssent_def, Receiver.rsent_def,Receiver.rrcvd_def]) 1);
 
-by(simp_tac (simpset() delsimps [trans_of_par4]
+by (simp_tac (simpset() delsimps [trans_of_par4]
                 addsimps [fork_lemma,inv1_def]) 1);
 
 (* Split proof in two *)
 by (rtac conjI 1); 
 
 (* First half *)
-by(asm_full_simp_tac (simpset() addsimps [Impl.inv1_def]) 1);
+by (asm_full_simp_tac (simpset() addsimps [Impl.inv1_def]) 1);
 by (rtac Action.action.induct 1);
 
 by (EVERY1[tac, tac, tac, tac]);
 by (tac 1);
 by (tac_ren 1);

 
 by (tac 1);
 by (tac_ren 1);
 
 (* 4 + 1 *)
-by(EVERY1[tac, tac, tac, tac]);
+by (EVERY1[tac, tac, tac, tac]);
 
 
 (* Now the other half *)
-by(asm_full_simp_tac (simpset() addsimps [Impl.inv1_def]) 1);
+by (asm_full_simp_tac (simpset() addsimps [Impl.inv1_def]) 1);
 by (rtac Action.action.induct 1);
-by(EVERY1[tac, tac]);
+by (EVERY1[tac, tac]);
 
 (* detour 1 *)
 by (tac 1);
 by (tac_ren 1);
 by (rtac impI 1);

 val tac2 = asm_full_simp_tac (ss addsimps [inv2_def]);
 
   (* 10 - 7 *)
   by (EVERY1[tac2,tac2,tac2,tac2]);
   (* 6 *)
-  by(forward_tac [rewrite_rule [Impl.inv1_def]
+  by (forward_tac [rewrite_rule [Impl.inv1_def]
                                (inv1 RS invariantE) RS conjunct1] 1);
   (* 6 - 5 *)
   by (EVERY1[tac2,tac2]);
 
   (* 4 *)

   by (fold_tac [rewrite_rule [Packet.hdr_def]Impl.hdr_sum_def]);
   by (fast_tac (claset() addDs [add_leD1,leD]) 1);
 
   (* 2 *)
   by (tac2 1);
-  by(forward_tac [rewrite_rule [Impl.inv1_def]
+  by (forward_tac [rewrite_rule [Impl.inv1_def]
                                (inv1 RS invariantE) RS conjunct1] 1);
   by (rtac impI 1);
   by (rtac impI 1);
   by (REPEAT (etac conjE 1));
   by (dres_inst_tac [("k","count (rsch s) (~sbit(sen s))")] le_imp_add_le 1);
   by (Asm_full_simp_tac 1);
 
   (* 1 *)
   by (tac2 1);
-  by(forward_tac [rewrite_rule [Impl.inv1_def]
+  by (forward_tac [rewrite_rule [Impl.inv1_def]
                                (inv1 RS invariantE) RS conjunct2] 1);
   by (rtac impI 1);
   by (rtac impI 1);
   by (REPEAT (etac conjE 1));
   by (fold_tac  [rewrite_rule[Packet.hdr_def]Impl.hdr_sum_def]);

   by (EVERY1[tac4,tac4,tac4,tac4,tac4,tac4,tac4,tac4,tac4]);
  
  (* 2 b *)
  
   by (strip_tac  1 THEN REPEAT (etac conjE 1));
-  by(forward_tac [rewrite_rule [Impl.inv2_def]
+  by (forward_tac [rewrite_rule [Impl.inv2_def]
                                (inv2 RS invariantE)] 1);
   by (tac4 1);
   by (Asm_full_simp_tac 1);
 
   (* 1 *)
   by (tac4 1);
   by (strip_tac  1 THEN REPEAT (etac conjE 1));
   by (rtac ccontr 1);
-  by(forward_tac [rewrite_rule [Impl.inv2_def]
+  by (forward_tac [rewrite_rule [Impl.inv2_def]
                                (inv2 RS invariantE)] 1);
-  by(forward_tac [rewrite_rule [Impl.inv3_def]
+  by (forward_tac [rewrite_rule [Impl.inv3_def]
                                (inv3 RS invariantE)] 1);
   by (Asm_full_simp_tac 1);
   by (eres_inst_tac [("x","m")] allE 1);
   by (dtac less_le_trans 1);
   by (dtac add_leD1 1);