src/HOLCF/ex/Hoare.ML

         (contr_tac 1),
         (fast_tac HOL_cs 1)
         ]);
 
 val hoare_lemma3 = prove_goal HOLCF.thy 
-" (!k.b1`(iterate k g x) = TT) | (? k. b1`(iterate k g x)~=TT)"
+" (!k. b1`(iterate k g x) = TT) | (? k. b1`(iterate k g x)~=TT)"
  (fn prems =>
         [
         (fast_tac HOL_cs 1)
         ]);
 

  p`(iterate ?k3 g ?x1) = p`?x1" : thm
 
 *)
 
 val hoare_lemma11 = prove_goal Hoare.thy 
-"(? n.b1`(iterate n g x) ~= TT) ==>\
-\ k=Least(%n.b1`(iterate n g x) ~= TT) & b1`(iterate k g x)=FF \
+"(? n. b1`(iterate n g x) ~= TT) ==>\
+\ k=Least(%n. b1`(iterate n g x) ~= TT) & b1`(iterate k g x)=FF \
 \ --> p`x = iterate k g x"
  (fn prems =>
         [
         (cut_facts_tac prems 1),
         (res_inst_tac [("n","k")] natE 1),