author | aspinall |
Wed, 13 Jul 2005 20:07:01 +0200 | |
changeset 16821 | ba1f6aba44ed |
parent 16625 | 53d4e0f2839b |
child 16922 | 2128ac2aa5db |
permissions | -rw-r--r-- |
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
1 |
|
15565 | 2 |
(* legacy ML bindings *) |
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
3 |
|
16204
5dd79d3f0105
renamed theorems monofun, contlub, cont to monofun_def, etc.; changed intro/elim rules for these predicates into more useful rule_format; removed all MF2 lemmas (Pcpo.thy has more general versions now); cleaned up many proofs.
huffman
parents:
15565
diff
changeset
|
4 |
val monofun_def = thm "monofun_def"; |
5dd79d3f0105
renamed theorems monofun, contlub, cont to monofun_def, etc.; changed intro/elim rules for these predicates into more useful rule_format; removed all MF2 lemmas (Pcpo.thy has more general versions now); cleaned up many proofs.
huffman
parents:
15565
diff
changeset
|
5 |
val contlub_def = thm "contlub_def"; |
5dd79d3f0105
renamed theorems monofun, contlub, cont to monofun_def, etc.; changed intro/elim rules for these predicates into more useful rule_format; removed all MF2 lemmas (Pcpo.thy has more general versions now); cleaned up many proofs.
huffman
parents:
15565
diff
changeset
|
6 |
val cont_def = thm "cont_def"; |
15565 | 7 |
val contlubI = thm "contlubI"; |
8 |
val contlubE = thm "contlubE"; |
|
9 |
val contI = thm "contI"; |
|
10 |
val contE = thm "contE"; |
|
11 |
val monofunI = thm "monofunI"; |
|
12 |
val monofunE = thm "monofunE"; |
|
13 |
val ch2ch_monofun = thm "ch2ch_monofun"; |
|
14 |
val ub2ub_monofun = thm "ub2ub_monofun"; |
|
15 |
val monocontlub2cont = thm "monocontlub2cont"; |
|
16 |
val binchain_cont = thm "binchain_cont"; |
|
17 |
val cont2mono = thm "cont2mono"; |
|
18 |
val cont2contlub = thm "cont2contlub"; |
|
19 |
val monofun_finch2finch = thm "monofun_finch2finch"; |
|
20 |
val cont_finch2finch = thm "cont_finch2finch"; |
|
21 |
val monofun_fun_fun = thm "monofun_fun_fun"; |
|
22 |
val monofun_fun_arg = thm "monofun_fun_arg"; |
|
23 |
val mono2mono_MF1L = thm "mono2mono_MF1L"; |
|
24 |
val cont2cont_CF1L = thm "cont2cont_CF1L"; |
|
25 |
val mono2mono_MF1L_rev = thm "mono2mono_MF1L_rev"; |
|
26 |
val cont2cont_CF1L_rev = thm "cont2cont_CF1L_rev"; |
|
16388
1ff571813848
renamed theorem cont2cont_CF1L_rev2 to cont2cont_lambda
huffman
parents:
16204
diff
changeset
|
27 |
val cont2cont_lambda = thm "cont2cont_lambda"; |
15565 | 28 |
val contlub_abstraction = thm "contlub_abstraction"; |
29 |
val mono2mono_app = thm "mono2mono_app"; |
|
30 |
val cont2contlub_app = thm "cont2contlub_app"; |
|
31 |
val cont2cont_app = thm "cont2cont_app"; |
|
32 |
val cont2cont_app2 = thm "cont2cont_app2"; |
|
33 |
val cont_id = thm "cont_id"; |
|
34 |
val cont_const = thm "cont_const"; |
|
35 |
val cont2cont_app3 = thm "cont2cont_app3"; |
|
36 |
val chfindom_monofun2cont = thm "chfindom_monofun2cont"; |
|
16625 | 37 |
val flatdom_strict2mono = thm "flatdom_strict2mono"; |
15565 | 38 |
val flatdom_strict2cont = thm "flatdom_strict2cont"; |