src/HOLCF/Porder.ML
author huffman
Sat, 04 Jun 2005 00:22:08 +0200
changeset 16221 879400e029bf
parent 15576 efb95d0d01f7
child 16922 2128ac2aa5db
permissions -rw-r--r--
New theory with lemmas for the fixrec package
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
     1
15562
8455c9671494 converted to new-style theory
huffman
parents: 14981
diff changeset
     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
8455c9671494 converted to new-style theory
huffman
parents: 14981
diff changeset
    11
val is_ub_def = thm "is_ub_def";
8455c9671494 converted to new-style theory
huffman
parents: 14981
diff changeset
    12
val is_lub_def = thm "is_lub_def";
8455c9671494 converted to new-style theory
huffman
parents: 14981
diff changeset
    13
val tord_def = thm "tord_def";
8455c9671494 converted to new-style theory
huffman
parents: 14981
diff changeset
    14
val chain_def = thm "chain_def";
8455c9671494 converted to new-style theory
huffman
parents: 14981
diff changeset
    15
val max_in_chain_def = thm "max_in_chain_def";
8455c9671494 converted to new-style theory
huffman
parents: 14981
diff changeset
    16
val finite_chain_def = thm "finite_chain_def";
8455c9671494 converted to new-style theory
huffman
parents: 14981
diff changeset
    17
val lub_def = thm "lub_def";
8455c9671494 converted to new-style theory
huffman
parents: 14981
diff changeset
    18
val unique_lub = thm "unique_lub";
8455c9671494 converted to new-style theory
huffman
parents: 14981
diff changeset
    19
val chain_mono = thm "chain_mono";
8455c9671494 converted to new-style theory
huffman
parents: 14981
diff changeset
    20
val chain_mono3 = thm "chain_mono3";
8455c9671494 converted to new-style theory
huffman
parents: 14981
diff changeset
    21
val chain_tord = thm "chain_tord";
8455c9671494 converted to new-style theory
huffman
parents: 14981
diff changeset
    22
val lub = thm "lub";
8455c9671494 converted to new-style theory
huffman
parents: 14981
diff changeset
    23
val lubI = thm "lubI";
8455c9671494 converted to new-style theory
huffman
parents: 14981
diff changeset
    24
val thelubI = thm "thelubI";
8455c9671494 converted to new-style theory
huffman
parents: 14981
diff changeset
    25
val lub_singleton = thm "lub_singleton";
8455c9671494 converted to new-style theory
huffman
parents: 14981
diff changeset
    26
val is_lubD1 = thm "is_lubD1";
8455c9671494 converted to new-style theory
huffman
parents: 14981
diff changeset
    27
val is_lub_lub = thm "is_lub_lub";
8455c9671494 converted to new-style theory
huffman
parents: 14981
diff changeset
    28
val is_lubI = thm "is_lubI";
8455c9671494 converted to new-style theory
huffman
parents: 14981
diff changeset
    29
val chainE = thm "chainE";
8455c9671494 converted to new-style theory
huffman
parents: 14981
diff changeset
    30
val chainI = thm "chainI";
8455c9671494 converted to new-style theory
huffman
parents: 14981
diff changeset
    31
val chain_shift = thm "chain_shift";
8455c9671494 converted to new-style theory
huffman
parents: 14981
diff changeset
    32
val ub_rangeD = thm "ub_rangeD";
8455c9671494 converted to new-style theory
huffman
parents: 14981
diff changeset
    33
val ub_rangeI = thm "ub_rangeI";
8455c9671494 converted to new-style theory
huffman
parents: 14981
diff changeset
    34
val is_ub_lub = thm "is_ub_lub";
8455c9671494 converted to new-style theory
huffman
parents: 14981
diff changeset
    35
val lub_finch1 = thm "lub_finch1";
8455c9671494 converted to new-style theory
huffman
parents: 14981
diff changeset
    36
val lub_finch2 = thm "lub_finch2";
8455c9671494 converted to new-style theory
huffman
parents: 14981
diff changeset
    37
val bin_chain = thm "bin_chain";
8455c9671494 converted to new-style theory
huffman
parents: 14981
diff changeset
    38
val bin_chainmax = thm "bin_chainmax";
8455c9671494 converted to new-style theory
huffman
parents: 14981
diff changeset
    39
val lub_bin_chain = thm "lub_bin_chain";
8455c9671494 converted to new-style theory
huffman
parents: 14981
diff changeset
    40
val lub_chain_maxelem = thm "lub_chain_maxelem";
8455c9671494 converted to new-style theory
huffman
parents: 14981
diff changeset
    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
8455c9671494 converted to new-style theory
huffman
parents: 14981
diff changeset
    43
structure Porder =
8455c9671494 converted to new-style theory
huffman
parents: 14981
diff changeset
    44
struct
8455c9671494 converted to new-style theory
huffman
parents: 14981
diff changeset
    45
  val thy = the_context ();
8455c9671494 converted to new-style theory
huffman
parents: 14981
diff changeset
    46
  val is_ub_def = is_ub_def;
8455c9671494 converted to new-style theory
huffman
parents: 14981
diff changeset
    47
  val is_lub_def = is_lub_def;
8455c9671494 converted to new-style theory
huffman
parents: 14981
diff changeset
    48
  val tord_def = tord_def;
8455c9671494 converted to new-style theory
huffman
parents: 14981
diff changeset
    49
  val chain_def = chain_def;
8455c9671494 converted to new-style theory
huffman
parents: 14981
diff changeset
    50
  val max_in_chain_def = max_in_chain_def;
8455c9671494 converted to new-style theory
huffman
parents: 14981
diff changeset
    51
  val finite_chain_def = finite_chain_def;
8455c9671494 converted to new-style theory
huffman
parents: 14981
diff changeset
    52
  val lub_def = lub_def;
8455c9671494 converted to new-style theory
huffman
parents: 14981
diff changeset
    53
end;