src/HOL/IOA/NTP/Correctness.ML

--- a/src/HOL/IOA/NTP/Correctness.ML	Fri Jan 17 10:09:46 1997 +0100
+++ b/src/HOL/IOA/NTP/Correctness.ML	Fri Jan 17 11:09:19 1997 +0100
@@ -39,12 +39,12 @@
 \   | C_m_r => False          \
 \   | C_r_s => False          \
 \   | C_r_r(m) => False)";
- by(simp_tac (!simpset addsimps ([externals_def, restrict_def,
+ by (simp_tac (!simpset addsimps ([externals_def, restrict_def,
                             restrict_asig_def, Spec.sig_def]
                             @asig_projections)) 1);
 
-  by(Action.action.induct_tac "a" 1);
-  by(ALLGOALS(simp_tac (!simpset addsimps [actions_def]@asig_projections)));
+  by (Action.action.induct_tac "a" 1);
+  by (ALLGOALS(simp_tac (!simpset addsimps [actions_def]@asig_projections)));
  (* 2 *)
   by (simp_tac (!simpset addsimps impl_ioas) 1);
   by (simp_tac (!simpset addsimps impl_asigs) 1);
@@ -67,52 +67,49 @@
 (* Proof of correctness *)
 goalw Correctness.thy [Spec.ioa_def, Solve.is_weak_pmap_def]
   "is_weak_pmap hom (restrict impl_ioa (externals spec_sig)) spec_ioa";
-by(simp_tac (!simpset addsimps 
-    [Correctness.hom_def,
-     cancel_restrict,externals_lemma]) 1);
+by (simp_tac (!simpset addsimps 
+    [Correctness.hom_def, cancel_restrict, externals_lemma]) 1);
 by (rtac conjI 1);
-by(simp_tac ss' 1);
-by (rtac ballI 1);
-by (dtac CollectD 1);
-by(asm_simp_tac (!simpset addsimps sels) 1);
-by(REPEAT(rtac allI 1));
+by (simp_tac ss' 1);
+by (asm_simp_tac (!simpset addsimps sels) 1);
+by (REPEAT(rtac allI 1));
 by (rtac imp_conj_lemma 1);   (* from lemmas.ML *)
 
-by(Action.action.induct_tac "a"  1);
-by(asm_simp_tac (ss' setloop (split_tac [expand_if])) 1);
-by(forward_tac [inv4] 1);
+by (Action.action.induct_tac "a"  1);
+by (asm_simp_tac (ss' setloop (split_tac [expand_if])) 1);
+by (forward_tac [inv4] 1);
 by (fast_tac (!claset addss (!simpset addsimps [neq_Nil_conv])) 1);
-by(simp_tac ss' 1);
-by(simp_tac ss' 1);
-by(simp_tac ss' 1);
-by(simp_tac ss' 1);
-by(simp_tac ss' 1);
-by(simp_tac ss' 1);
-by(simp_tac ss' 1);
+by (simp_tac ss' 1);
+by (simp_tac ss' 1);
+by (simp_tac ss' 1);
+by (simp_tac ss' 1);
+by (simp_tac ss' 1);
+by (simp_tac ss' 1);
+by (simp_tac ss' 1);
 
-by(asm_simp_tac ss' 1);
-by(forward_tac [inv4] 1);
-by(forward_tac [inv2] 1);
+by (asm_simp_tac ss' 1);
+by (forward_tac [inv4] 1);
+by (forward_tac [inv2] 1);
 by (etac disjE 1);
-by(Asm_simp_tac 1);
+by (Asm_simp_tac 1);
 by (fast_tac (!claset addss (!simpset addsimps [neq_Nil_conv])) 1);
 
-by(asm_simp_tac ss' 1);
-by(forward_tac [inv2] 1);
+by (asm_simp_tac ss' 1);
+by (forward_tac [inv2] 1);
 by (etac disjE 1);
 
-by(forward_tac [inv3] 1);
-by(case_tac "sq(sen(s))=[]" 1);
+by (forward_tac [inv3] 1);
+by (case_tac "sq(sen(s))=[]" 1);
 
-by(asm_full_simp_tac ss' 1);
-by(fast_tac (!claset addSDs [add_leD1 RS leD]) 1);
+by (asm_full_simp_tac ss' 1);
+by (fast_tac (!claset addSDs [add_leD1 RS leD]) 1);
 
-by(case_tac "m = hd(sq(sen(s)))" 1);
+by (case_tac "m = hd(sq(sen(s)))" 1);
 
 by (fast_tac (!claset addss (!simpset addsimps [neq_Nil_conv])) 1);
 
-by(Asm_full_simp_tac 1);
-by(fast_tac (!claset addSDs [add_leD1 RS leD]) 1);
+by (Asm_full_simp_tac 1);
+by (fast_tac (!claset addSDs [add_leD1 RS leD]) 1);
 
-by(Asm_full_simp_tac 1);
+by (Asm_full_simp_tac 1);
 qed"ntp_correct";