src/HOLCF/Lift2.ML

 *)
 
 open Lift2;
 
 (* for compatibility with old HOLCF-Version *)
-qed_goal "inst_lift_po" thy "(op <<)=(%x y.x=y|x=Undef)"
+qed_goal "inst_lift_po" thy "(op <<)=(%x y. x=y|x=Undef)"
  (fn prems => 
         [
         (fold_goals_tac [less_lift_def]),
         (rtac refl 1)
         ]);

 by (simp_tac (!simpset addsimps [inst_lift_po]) 1);
 qed"minimal_lift";
 
 bind_thm ("UU_lift_def",minimal_lift RS minimal2UU RS sym);
 
-qed_goal "least_lift" thy "? x::'a lift.!y.x<<y"
+qed_goal "least_lift" thy "? x::'a lift.!y. x<<y"
 (fn prems =>
         [
         (res_inst_tac [("x","Undef")] exI 1),
         (rtac (minimal_lift RS allI) 1)
         ]);

 
 (* Tailoring chain_mono2 of Pcpo.ML to Undef *)
 
 goal Lift2.thy
 "!!Y. [|? j.~Y(j)=Undef;is_chain(Y::nat=>('a)lift)|] \
-\ ==> ? j.!i.j<i-->~Y(i)=Undef";
+\ ==> ? j.!i. j<i-->~Y(i)=Undef";
 by Safe_tac;
 by (Step_tac 1);
 by (strip_tac 1);
 by (rtac notUndef_I 1);
 by (atac 2);

 
 goal Lift2.thy
         "(! Y. is_chain(Y::nat=>('a)lift)-->(? n. max_in_chain n Y))";
 by (rewtac max_in_chain_def);  
 by (strip_tac 1);
-by (res_inst_tac [("P","!i.Y(i)=Undef")] case_split_thm  1);
+by (res_inst_tac [("P","!i. Y(i)=Undef")] case_split_thm  1);
 by (res_inst_tac [("x","0")] exI 1);
 by (strip_tac 1);
 by (rtac trans 1);
 by (etac spec 1);
 by (rtac sym 1);
 by (etac spec 1); 
 
-by (subgoal_tac "!x y.x<<(y::('a)lift) --> x=Undef | x=y" 1);
+by (subgoal_tac "!x y. x<<(y::('a)lift) --> x=Undef | x=y" 1);
 by (simp_tac (!simpset addsimps [inst_lift_po]) 2);
 by (rtac (chain_mono2_po RS exE) 1); 
 by (Fast_tac 1); 
 by (atac 1); 
 by (res_inst_tac [("x","Suc(x)")] exI 1); 

 
 
 (* Main Lemma: cpo_lift *)
 
 goal Lift2.thy  
-  "!!Y. is_chain(Y::nat=>('a)lift) ==> ? x.range(Y) <<|x";
+  "!!Y. is_chain(Y::nat=>('a)lift) ==> ? x. range(Y) <<|x";
 by (cut_inst_tac [] flat_imp_chain_finite_poo 1);
 by (Step_tac 1);
 by Safe_tac;
 by (Step_tac 1); 
 by (rtac exI 1);