src/HOLCF/Cfun1.ML
changeset 3323 194ae2e0c193
parent 2838 2e908f29bc3d
child 5291 5706f0ef1d43
     1.1 --- a/src/HOLCF/Cfun1.ML	Fri May 23 18:55:28 1997 +0200
     1.2 +++ b/src/HOLCF/Cfun1.ML	Sun May 25 11:07:52 1997 +0200
     1.3 @@ -35,14 +35,14 @@
     1.4  (* less_cfun is a partial order on type 'a -> 'b                            *)
     1.5  (* ------------------------------------------------------------------------ *)
     1.6  
     1.7 -qed_goalw "refl_less_cfun" thy [less_cfun_def] "less(f::'a->'b) f"
     1.8 +qed_goalw "refl_less_cfun" thy [less_cfun_def] "(f::'a->'b) << f"
     1.9  (fn prems =>
    1.10          [
    1.11          (rtac refl_less 1)
    1.12          ]);
    1.13  
    1.14  qed_goalw "antisym_less_cfun" thy [less_cfun_def] 
    1.15 -        "[|less (f1::'a->'b) f2; less f2 f1|] ==> f1 = f2"
    1.16 +        "[|(f1::'a->'b) << f2; f2 << f1|] ==> f1 = f2"
    1.17  (fn prems =>
    1.18          [
    1.19          (cut_facts_tac prems 1),
    1.20 @@ -55,7 +55,7 @@
    1.21          ]);
    1.22  
    1.23  qed_goalw "trans_less_cfun" thy [less_cfun_def] 
    1.24 -        "[|less (f1::'a->'b) f2; less f2 f3|] ==> less f1 f3"
    1.25 +        "[|(f1::'a->'b) << f2; f2 << f3|] ==> f1 << f3"
    1.26  (fn prems =>
    1.27          [
    1.28          (cut_facts_tac prems 1),