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/Ffun.ML
author wenzelm
Tue, 21 Jun 2005 09:51:59 +0200
changeset 16513 f38693aad717
parent 16202 61811f31ce5a
child 16922 2128ac2aa5db
permissions -rw-r--r--
enter_thms: use theorem database of thy *after* attribute application;


(* legacy ML bindings *)

val less_fun_def = thm "less_fun_def";
val refl_less_fun = thm "refl_less_fun";
val antisym_less_fun = thm "antisym_less_fun";
val trans_less_fun = thm "trans_less_fun";
val minimal_fun = thm "minimal_fun";
val least_fun = thm "least_fun";
val less_fun = thm "less_fun";
val ch2ch_fun = thm "ch2ch_fun";
val ub2ub_fun = thm "ub2ub_fun";
val lub_fun = thm "lub_fun";
val thelub_fun = thm "thelub_fun";
val cpo_fun = thm "cpo_fun";
val inst_fun_pcpo = thm "inst_fun_pcpo";
isabelle