src/HOLCF/Cfun1.ML
changeset 10834 a7897aebbffc
parent 9248 e1dee89de037
child 12030 46d57d0290a2
     1.1 --- a/src/HOLCF/Cfun1.ML	Tue Jan 09 15:29:17 2001 +0100
     1.2 +++ b/src/HOLCF/Cfun1.ML	Tue Jan 09 15:32:27 2001 +0100
     1.3 @@ -50,15 +50,15 @@
     1.4  (* lemmas about application of continuous functions                         *)
     1.5  (* ------------------------------------------------------------------------ *)
     1.6  
     1.7 -Goal "[| f=g; x=y |] ==> f`x = g`y";
     1.8 +Goal "[| f=g; x=y |] ==> f$x = g$y";
     1.9  by (Asm_simp_tac 1);
    1.10  qed "cfun_cong";
    1.11  
    1.12 -Goal "f=g ==> f`x = g`x";
    1.13 +Goal "f=g ==> f$x = g$x";
    1.14  by (Asm_simp_tac 1);
    1.15  qed "cfun_fun_cong";
    1.16  
    1.17 -Goal "x=y ==> f`x = f`y";
    1.18 +Goal "x=y ==> f$x = f$y";
    1.19  by (Asm_simp_tac 1);
    1.20  qed "cfun_arg_cong";
    1.21  
    1.22 @@ -77,7 +77,7 @@
    1.23  (* simplification of application                                            *)
    1.24  (* ------------------------------------------------------------------------ *)
    1.25  
    1.26 -Goal "cont f ==> (Abs_CFun f)`x = f x";
    1.27 +Goal "cont f ==> (Abs_CFun f)$x = f x";
    1.28  by (etac (Abs_Cfun_inverse2 RS fun_cong) 1);
    1.29  qed "Cfunapp2";
    1.30  
    1.31 @@ -85,7 +85,7 @@
    1.32  (* beta - equality for continuous functions                                 *)
    1.33  (* ------------------------------------------------------------------------ *)
    1.34  
    1.35 -Goal "cont(c1) ==> (LAM x .c1 x)`u = c1 u";
    1.36 +Goal "cont(c1) ==> (LAM x .c1 x)$u = c1 u";
    1.37  by (rtac Cfunapp2 1);
    1.38  by (atac 1);
    1.39  qed "beta_cfun";