| author | huffman | 
| Tue, 26 Jul 2005 18:27:16 +0200 | |
| changeset 16920 | ded12c9e88c2 | 
| parent 16202 | 61811f31ce5a | 
| child 16922 | 2128ac2aa5db | 
| permissions | -rw-r--r-- | 
(* 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";