src/HOLCF/Ssum3.ML

 (* ------------------------------------------------------------------------ *)
 (* first 5 ugly lemmas                                                      *)
 (* ------------------------------------------------------------------------ *)
 
 qed_goal "ssum_lemma9" Ssum3.thy 
-"[| is_chain(Y); lub(range(Y)) = Isinl(x)|] ==> !i.? x.Y(i)=Isinl(x)"
+"[| is_chain(Y); lub(range(Y)) = Isinl(x)|] ==> !i.? x. Y(i)=Isinl(x)"
  (fn prems =>
         [
         (cut_facts_tac prems 1),
         (strip_tac 1),
         (res_inst_tac [("p","Y(i)")] IssumE 1),

         (etac is_ub_thelub 1)
         ]);
 
 
 qed_goal "ssum_lemma10" Ssum3.thy 
-"[| is_chain(Y); lub(range(Y)) = Isinr(x)|] ==> !i.? x.Y(i)=Isinr(x)"
+"[| is_chain(Y); lub(range(Y)) = Isinr(x)|] ==> !i.? x. Y(i)=Isinr(x)"
  (fn prems =>
         [
         (cut_facts_tac prems 1),
         (strip_tac 1),
         (res_inst_tac [("p","Y(i)")] IssumE 1),

         (asm_simp_tac (Ssum0_ss addsimps [cont_Isinl]) 1)
         ]);
 
 qed_goalw "thelub_ssum2b" Ssum3.thy [sinl_def,sinr_def,sswhen_def] 
 "[| is_chain(Y); !i.? x. Y(i) = sinr`x |] ==>\ 
-\   lub(range(Y)) = sinr`(lub(range(%i. sswhen`(LAM y. UU)`(LAM x.x)`(Y i))))"
+\   lub(range(Y)) = sinr`(lub(range(%i. sswhen`(LAM y. UU)`(LAM x. x)`(Y i))))"
  (fn prems =>
         [
         (cut_facts_tac prems 1),
         (stac beta_cfun 1),
 	tac,

         [cont_Isinr,cont_Isinl,cont_Iwhen1,cont_Iwhen2,
         cont_Iwhen3]) 1)
         ]);
 
 qed_goalw "thelub_ssum2a_rev" Ssum3.thy [sinl_def,sinr_def] 
-        "[| is_chain(Y); lub(range(Y)) = sinl`x|] ==> !i.? x.Y(i)=sinl`x"
+        "[| is_chain(Y); lub(range(Y)) = sinl`x|] ==> !i.? x. Y(i)=sinl`x"
  (fn prems =>
         [
         (cut_facts_tac prems 1),
         (asm_simp_tac (Ssum0_ss addsimps 
         [cont_Isinr,cont_Isinl,cont_Iwhen1,cont_Iwhen2,

         [cont_Isinr,cont_Isinl,cont_Iwhen1,cont_Iwhen2,
         cont_Iwhen3]) 1)
         ]);
 
 qed_goalw "thelub_ssum2b_rev" Ssum3.thy [sinl_def,sinr_def] 
-        "[| is_chain(Y); lub(range(Y)) = sinr`x|] ==> !i.? x.Y(i)=sinr`x"
+        "[| is_chain(Y); lub(range(Y)) = sinr`x|] ==> !i.? x. Y(i)=sinr`x"
  (fn prems =>
         [
         (cut_facts_tac prems 1),
         (asm_simp_tac (Ssum0_ss addsimps 
         [cont_Isinr,cont_Isinl,cont_Iwhen1,cont_Iwhen2,

         cont_Iwhen3]) 1)
         ]);
 
 qed_goal "thelub_ssum3" Ssum3.thy  
 "is_chain(Y) ==>\ 
-\   lub(range(Y)) = sinl`(lub(range(%i. sswhen`(LAM x. x)`(LAM y.UU)`(Y i))))\
-\ | lub(range(Y)) = sinr`(lub(range(%i. sswhen`(LAM y. UU)`(LAM x.x)`(Y i))))"
+\   lub(range(Y)) = sinl`(lub(range(%i. sswhen`(LAM x. x)`(LAM y. UU)`(Y i))))\
+\ | lub(range(Y)) = sinr`(lub(range(%i. sswhen`(LAM y. UU)`(LAM x. x)`(Y i))))"
  (fn prems =>
         [
         (cut_facts_tac prems 1),
         (rtac (ssum_chainE RS disjE) 1),
         (atac 1),