src/HOLCF/Tr.ML
author huffman
Sat, 04 Jun 2005 00:22:08 +0200
changeset 16221 879400e029bf
parent 15649 f8345ee4f607
child 16756 e05c8039873a
permissions -rw-r--r--
New theory with lemmas for the fixrec package
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
2640
ee4dfce170a0 Changes of HOLCF from Oscar Slotosch:
slotosch
parents:
diff changeset
     1
15649
f8345ee4f607 convert to new-style theory
huffman
parents: 14981
diff changeset
     2
(* legacy ML bindings *)
2640
ee4dfce170a0 Changes of HOLCF from Oscar Slotosch:
slotosch
parents:
diff changeset
     3
15649
f8345ee4f607 convert to new-style theory
huffman
parents: 14981
diff changeset
     4
val TT_def = thm "TT_def";
f8345ee4f607 convert to new-style theory
huffman
parents: 14981
diff changeset
     5
val FF_def = thm "FF_def";
f8345ee4f607 convert to new-style theory
huffman
parents: 14981
diff changeset
     6
val neg_def = thm "neg_def";
f8345ee4f607 convert to new-style theory
huffman
parents: 14981
diff changeset
     7
val ifte_def = thm "ifte_def";
f8345ee4f607 convert to new-style theory
huffman
parents: 14981
diff changeset
     8
val andalso_def = thm "andalso_def";
f8345ee4f607 convert to new-style theory
huffman
parents: 14981
diff changeset
     9
val orelse_def = thm "orelse_def";
f8345ee4f607 convert to new-style theory
huffman
parents: 14981
diff changeset
    10
val If2_def = thm "If2_def";
f8345ee4f607 convert to new-style theory
huffman
parents: 14981
diff changeset
    11
val Exh_tr = thm "Exh_tr";
f8345ee4f607 convert to new-style theory
huffman
parents: 14981
diff changeset
    12
val trE = thm "trE";
f8345ee4f607 convert to new-style theory
huffman
parents: 14981
diff changeset
    13
val tr_defs = thms "tr_defs";
f8345ee4f607 convert to new-style theory
huffman
parents: 14981
diff changeset
    14
val dist_less_tr = thms "dist_less_tr";
f8345ee4f607 convert to new-style theory
huffman
parents: 14981
diff changeset
    15
val dist_eq_tr = thms "dist_eq_tr";
f8345ee4f607 convert to new-style theory
huffman
parents: 14981
diff changeset
    16
val ifte_simp = thm "ifte_simp";
f8345ee4f607 convert to new-style theory
huffman
parents: 14981
diff changeset
    17
val ifte_thms = thms "ifte_thms";
f8345ee4f607 convert to new-style theory
huffman
parents: 14981
diff changeset
    18
val andalso_thms = thms "andalso_thms";
f8345ee4f607 convert to new-style theory
huffman
parents: 14981
diff changeset
    19
val orelse_thms = thms "orelse_thms";
f8345ee4f607 convert to new-style theory
huffman
parents: 14981
diff changeset
    20
val neg_thms = thms "neg_thms";
f8345ee4f607 convert to new-style theory
huffman
parents: 14981
diff changeset
    21
val split_If2 = thm "split_If2";
f8345ee4f607 convert to new-style theory
huffman
parents: 14981
diff changeset
    22
val andalso_or = thm "andalso_or";
f8345ee4f607 convert to new-style theory
huffman
parents: 14981
diff changeset
    23
val andalso_and = thm "andalso_and";
f8345ee4f607 convert to new-style theory
huffman
parents: 14981
diff changeset
    24
val Def_bool1 = thm "Def_bool1";
f8345ee4f607 convert to new-style theory
huffman
parents: 14981
diff changeset
    25
val Def_bool2 = thm "Def_bool2";
f8345ee4f607 convert to new-style theory
huffman
parents: 14981
diff changeset
    26
val Def_bool3 = thm "Def_bool3";
f8345ee4f607 convert to new-style theory
huffman
parents: 14981
diff changeset
    27
val Def_bool4 = thm "Def_bool4";
f8345ee4f607 convert to new-style theory
huffman
parents: 14981
diff changeset
    28
val If_and_if = thm "If_and_if";
f8345ee4f607 convert to new-style theory
huffman
parents: 14981
diff changeset
    29
val adm_trick_1 = thm "adm_trick_1";
f8345ee4f607 convert to new-style theory
huffman
parents: 14981
diff changeset
    30
val adm_trick_2 = thm "adm_trick_2";
f8345ee4f607 convert to new-style theory
huffman
parents: 14981
diff changeset
    31
val adm_tricks = thms "adm_tricks";
f8345ee4f607 convert to new-style theory
huffman
parents: 14981
diff changeset
    32
val adm_nTT = thm "adm_nTT";
f8345ee4f607 convert to new-style theory
huffman
parents: 14981
diff changeset
    33
val adm_nFF = thm "adm_nFF";
2640
ee4dfce170a0 Changes of HOLCF from Oscar Slotosch:
slotosch
parents:
diff changeset
    34