src/HOLCF/Ffun.ML
author huffman
Tue, 26 Jul 2005 18:29:59 +0200
changeset 16922 2128ac2aa5db
parent 16202 61811f31ce5a
child 17831 4a8c3f8b0a92
permissions -rw-r--r--
brought ML files up to date with new lemmas
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
16202
61811f31ce5a renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff changeset
     1
61811f31ce5a renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff changeset
     2
(* legacy ML bindings *)
61811f31ce5a renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff changeset
     3
61811f31ce5a renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff changeset
     4
val antisym_less_fun = thm "antisym_less_fun";
16922
2128ac2aa5db brought ML files up to date with new lemmas
huffman
parents: 16202
diff changeset
     5
val app_strict = thm "app_strict";
16202
61811f31ce5a renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff changeset
     6
val ch2ch_fun = thm "ch2ch_fun";
16922
2128ac2aa5db brought ML files up to date with new lemmas
huffman
parents: 16202
diff changeset
     7
val ch2ch_fun_rev = thm "ch2ch_fun_rev";
16202
61811f31ce5a renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff changeset
     8
val cpo_fun = thm "cpo_fun";
61811f31ce5a renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff changeset
     9
val inst_fun_pcpo = thm "inst_fun_pcpo";
16922
2128ac2aa5db brought ML files up to date with new lemmas
huffman
parents: 16202
diff changeset
    10
val least_fun = thm "least_fun";
2128ac2aa5db brought ML files up to date with new lemmas
huffman
parents: 16202
diff changeset
    11
val less_fun_def = thm "less_fun_def";
2128ac2aa5db brought ML files up to date with new lemmas
huffman
parents: 16202
diff changeset
    12
val less_fun_ext = thm "less_fun_ext";
2128ac2aa5db brought ML files up to date with new lemmas
huffman
parents: 16202
diff changeset
    13
val less_fun = thm "less_fun";
2128ac2aa5db brought ML files up to date with new lemmas
huffman
parents: 16202
diff changeset
    14
val lub_fun = thm "lub_fun";
2128ac2aa5db brought ML files up to date with new lemmas
huffman
parents: 16202
diff changeset
    15
val minimal_fun = thm "minimal_fun";
2128ac2aa5db brought ML files up to date with new lemmas
huffman
parents: 16202
diff changeset
    16
val refl_less_fun = thm "refl_less_fun";
2128ac2aa5db brought ML files up to date with new lemmas
huffman
parents: 16202
diff changeset
    17
val thelub_fun = thm "thelub_fun";
2128ac2aa5db brought ML files up to date with new lemmas
huffman
parents: 16202
diff changeset
    18
val trans_less_fun = thm "trans_less_fun";
2128ac2aa5db brought ML files up to date with new lemmas
huffman
parents: 16202
diff changeset
    19
val ub2ub_fun = thm "ub2ub_fun";
2128ac2aa5db brought ML files up to date with new lemmas
huffman
parents: 16202
diff changeset
    20