--- a/src/HOLCF/IMP/HoareEx.ML Tue Dec 16 15:17:26 1997 +0100
+++ b/src/HOLCF/IMP/HoareEx.ML Tue Dec 16 17:58:03 1997 +0100
@@ -8,12 +8,12 @@
val prems = goalw thy [hoare_valid_def]
"|= {A} c {A} ==> |= {A} WHILE b DO c {%s. A s & ~b s}";
-by(cut_facts_tac prems 1);
+by (cut_facts_tac prems 1);
by (Simp_tac 1);
by (rtac fix_ind 1);
(* simplifier with enhanced adm-tactic: *)
by (Simp_tac 1);
by (Simp_tac 1);
by (simp_tac (simpset() setloop (split_tac[expand_if])) 1);
-by(Blast_tac 1);
+by (Blast_tac 1);
qed "WHILE_rule_sound";