src/HOLCF/Cfun2.ML
changeset 3842 b55686a7b22c
parent 3323 194ae2e0c193
child 4098 71e05eb27fb6
     1.1 --- a/src/HOLCF/Cfun2.ML	Fri Oct 10 18:37:49 1997 +0200
     1.2 +++ b/src/HOLCF/Cfun2.ML	Fri Oct 10 19:02:28 1997 +0200
     1.3 @@ -9,7 +9,7 @@
     1.4  open Cfun2;
     1.5  
     1.6  (* for compatibility with old HOLCF-Version *)
     1.7 -qed_goal "inst_cfun_po" thy "(op <<)=(%f1 f2.fapp f1 << fapp f2)"
     1.8 +qed_goal "inst_cfun_po" thy "(op <<)=(%f1 f2. fapp f1 << fapp f2)"
     1.9   (fn prems => 
    1.10          [
    1.11  	(fold_goals_tac [less_cfun_def]),
    1.12 @@ -30,7 +30,7 @@
    1.13  (* Type 'a ->'b  is pointed                                                 *)
    1.14  (* ------------------------------------------------------------------------ *)
    1.15  
    1.16 -qed_goal "minimal_cfun" thy "fabs(% x.UU) << f"
    1.17 +qed_goal "minimal_cfun" thy "fabs(% x. UU) << f"
    1.18  (fn prems =>
    1.19          [
    1.20          (stac less_cfun 1),
    1.21 @@ -41,10 +41,10 @@
    1.22  
    1.23  bind_thm ("UU_cfun_def",minimal_cfun RS minimal2UU RS sym);
    1.24  
    1.25 -qed_goal "least_cfun" thy "? x::'a->'b::pcpo.!y.x<<y"
    1.26 +qed_goal "least_cfun" thy "? x::'a->'b::pcpo.!y. x<<y"
    1.27  (fn prems =>
    1.28          [
    1.29 -        (res_inst_tac [("x","fabs(% x.UU)")] exI 1),
    1.30 +        (res_inst_tac [("x","fabs(% x. UU)")] exI 1),
    1.31          (rtac (minimal_cfun RS allI) 1)
    1.32          ]);
    1.33  
    1.34 @@ -156,7 +156,7 @@
    1.35  (* ------------------------------------------------------------------------ *)
    1.36  
    1.37  qed_goal "lub_cfun_mono" thy 
    1.38 -        "is_chain(F) ==> monofun(% x.lub(range(% j.(F j)`x)))"
    1.39 +        "is_chain(F) ==> monofun(% x. lub(range(% j.(F j)`x)))"
    1.40  (fn prems =>
    1.41          [
    1.42          (cut_facts_tac prems 1),
    1.43 @@ -190,7 +190,7 @@
    1.44  (* ------------------------------------------------------------------------ *)
    1.45  
    1.46  qed_goal "cont_lubcfun" thy 
    1.47 -        "is_chain(F) ==> cont(% x.lub(range(% j.F(j)`x)))"
    1.48 +        "is_chain(F) ==> cont(% x. lub(range(% j. F(j)`x)))"
    1.49  (fn prems =>
    1.50          [
    1.51          (cut_facts_tac prems 1),
    1.52 @@ -209,7 +209,7 @@
    1.53  (* ------------------------------------------------------------------------ *)
    1.54  
    1.55  qed_goal "lub_cfun" thy 
    1.56 -  "is_chain(CCF) ==> range(CCF) <<| (LAM x.lub(range(% i.CCF(i)`x)))"
    1.57 +  "is_chain(CCF) ==> range(CCF) <<| (LAM x. lub(range(% i. CCF(i)`x)))"
    1.58  (fn prems =>
    1.59          [
    1.60          (cut_facts_tac prems 1),