Mercurial Mercurial > repos > isabelle / file revision
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOLCF/fun1.thy
author wenzelm
Thu, 15 Nov 2001 18:20:13 +0100
changeset 12207 4dff931b852f
parent 243 c22b85994e17
permissions -rw-r--r--
added Induct/Binary_Trees.thy, Induct/Tree_Forest (converted from former ex/TF.ML ex/TF.thy ex/Term.ML ex/Term.thy);

(*  Title: 	HOLCF/fun1.thy
    ID:         $Id$
    Author: 	Franz Regensburger
    Copyright   1993  Technische Universitaet Muenchen


Definition of the partial ordering for the type of all functions => (fun)

REMARK: The ordering on 'a => 'b is only defined if 'b is in class po !!

*)

Fun1 = Pcpo +

(* default class is still term *)

consts
  less_fun	:: "['a=>'b::po,'a=>'b] => bool"	

rules
   (* definition of the ordering less_fun            *)
   (* in fun1.ML it is proved that less_fun is a po *)
   
  less_fun_def "less_fun(f1,f2) == ! x. f1(x) << f2(x)"  

end
isabelle