author | wenzelm |
Fri, 15 Jul 2005 11:26:22 +0200 | |
changeset 16858 | fade1d3a2995 |
parent 15576 | efb95d0d01f7 |
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 |
|
15562 | 2 |
(* legacy ML bindings *) |
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
3 |
|
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
15562
diff
changeset
|
4 |
val refl_less = thm "refl_less"; |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
15562
diff
changeset
|
5 |
val antisym_less = thm "antisym_less"; |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
15562
diff
changeset
|
6 |
val trans_less = thm "trans_less"; |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
15562
diff
changeset
|
7 |
val minimal2UU = thm "minimal2UU"; |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
15562
diff
changeset
|
8 |
val antisym_less_inverse = thm "antisym_less_inverse"; |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
15562
diff
changeset
|
9 |
val box_less = thm "box_less"; |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
15562
diff
changeset
|
10 |
val po_eq_conv = thm "po_eq_conv"; |
15562 | 11 |
val is_ub_def = thm "is_ub_def"; |
12 |
val is_lub_def = thm "is_lub_def"; |
|
13 |
val tord_def = thm "tord_def"; |
|
14 |
val chain_def = thm "chain_def"; |
|
15 |
val max_in_chain_def = thm "max_in_chain_def"; |
|
16 |
val finite_chain_def = thm "finite_chain_def"; |
|
17 |
val lub_def = thm "lub_def"; |
|
18 |
val unique_lub = thm "unique_lub"; |
|
19 |
val chain_mono = thm "chain_mono"; |
|
20 |
val chain_mono3 = thm "chain_mono3"; |
|
21 |
val chain_tord = thm "chain_tord"; |
|
22 |
val lub = thm "lub"; |
|
23 |
val lubI = thm "lubI"; |
|
24 |
val thelubI = thm "thelubI"; |
|
25 |
val lub_singleton = thm "lub_singleton"; |
|
26 |
val is_lubD1 = thm "is_lubD1"; |
|
27 |
val is_lub_lub = thm "is_lub_lub"; |
|
28 |
val is_lubI = thm "is_lubI"; |
|
29 |
val chainE = thm "chainE"; |
|
30 |
val chainI = thm "chainI"; |
|
31 |
val chain_shift = thm "chain_shift"; |
|
32 |
val ub_rangeD = thm "ub_rangeD"; |
|
33 |
val ub_rangeI = thm "ub_rangeI"; |
|
34 |
val is_ub_lub = thm "is_ub_lub"; |
|
35 |
val lub_finch1 = thm "lub_finch1"; |
|
36 |
val lub_finch2 = thm "lub_finch2"; |
|
37 |
val bin_chain = thm "bin_chain"; |
|
38 |
val bin_chainmax = thm "bin_chainmax"; |
|
39 |
val lub_bin_chain = thm "lub_bin_chain"; |
|
40 |
val lub_chain_maxelem = thm "lub_chain_maxelem"; |
|
41 |
val lub_const = thm "lub_const"; |
|
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
42 |
|
15562 | 43 |
structure Porder = |
44 |
struct |
|
45 |
val thy = the_context (); |
|
46 |
val is_ub_def = is_ub_def; |
|
47 |
val is_lub_def = is_lub_def; |
|
48 |
val tord_def = tord_def; |
|
49 |
val chain_def = chain_def; |
|
50 |
val max_in_chain_def = max_in_chain_def; |
|
51 |
val finite_chain_def = finite_chain_def; |
|
52 |
val lub_def = lub_def; |
|
53 |
end; |