src/HOLCF/Sprod2.ML
changeset 3842 b55686a7b22c
parent 3323 194ae2e0c193
child 4031 42cbf6256d60
     1.1 --- a/src/HOLCF/Sprod2.ML	Fri Oct 10 18:37:49 1997 +0200
     1.2 +++ b/src/HOLCF/Sprod2.ML	Fri Oct 10 19:02:28 1997 +0200
     1.3 @@ -9,7 +9,7 @@
     1.4  open Sprod2;
     1.5  
     1.6  (* for compatibility with old HOLCF-Version *)
     1.7 -qed_goal "inst_sprod_po" thy "(op <<)=(%x y.Isfst x<<Isfst y&Issnd x<<Issnd y)"
     1.8 +qed_goal "inst_sprod_po" thy "(op <<)=(%x y. Isfst x<<Isfst y&Issnd x<<Issnd y)"
     1.9   (fn prems => 
    1.10          [
    1.11  	(fold_goals_tac [less_sprod_def]),
    1.12 @@ -28,7 +28,7 @@
    1.13  
    1.14  bind_thm ("UU_sprod_def",minimal_sprod RS minimal2UU RS sym);
    1.15  
    1.16 -qed_goal "least_sprod" thy "? x::'a**'b.!y.x<<y"
    1.17 +qed_goal "least_sprod" thy "? x::'a**'b.!y. x<<y"
    1.18  (fn prems =>
    1.19          [
    1.20          (res_inst_tac [("x","Ispair UU UU")] exI 1),
    1.21 @@ -96,7 +96,7 @@
    1.22  
    1.23  qed_goal "lub_sprod" Sprod2.thy 
    1.24  "[|is_chain(S)|] ==> range(S) <<| \
    1.25 -\ Ispair (lub(range(%i.Isfst(S i)))) (lub(range(%i.Issnd(S i))))"
    1.26 +\ Ispair (lub(range(%i. Isfst(S i)))) (lub(range(%i. Issnd(S i))))"
    1.27  (fn prems =>
    1.28          [
    1.29          (cut_facts_tac prems 1),
    1.30 @@ -123,7 +123,7 @@
    1.31  
    1.32  
    1.33  qed_goal "cpo_sprod" Sprod2.thy 
    1.34 -        "is_chain(S::nat=>'a**'b)==>? x.range(S)<<| x"
    1.35 +        "is_chain(S::nat=>'a**'b)==>? x. range(S)<<| x"
    1.36  (fn prems =>
    1.37          [
    1.38          (cut_facts_tac prems 1),