author | paulson |
Tue, 20 May 1997 11:49:57 +0200 | |
changeset 3245 | 241838c01caf |
parent 2112 | 3902e9af752f |
child 3302 | 404fe31fd8d2 |
permissions | -rw-r--r-- |
2112 | 1 |
signature Thms_sig = |
2 |
sig |
|
3245
241838c01caf
Removal of redundant code (unused or already present in Isabelle.
paulson
parents:
2112
diff
changeset
|
3 |
val WF_INDUCTION_THM:thm |
241838c01caf
Removal of redundant code (unused or already present in Isabelle.
paulson
parents:
2112
diff
changeset
|
4 |
val WFREC_COROLLARY :thm |
241838c01caf
Removal of redundant code (unused or already present in Isabelle.
paulson
parents:
2112
diff
changeset
|
5 |
val CUT_DEF :thm |
241838c01caf
Removal of redundant code (unused or already present in Isabelle.
paulson
parents:
2112
diff
changeset
|
6 |
val CUT_LEMMA :thm |
241838c01caf
Removal of redundant code (unused or already present in Isabelle.
paulson
parents:
2112
diff
changeset
|
7 |
val SELECT_AX :thm |
2112 | 8 |
|
3245
241838c01caf
Removal of redundant code (unused or already present in Isabelle.
paulson
parents:
2112
diff
changeset
|
9 |
val COND_CONG :thm |
241838c01caf
Removal of redundant code (unused or already present in Isabelle.
paulson
parents:
2112
diff
changeset
|
10 |
val LET_CONG :thm |
2112 | 11 |
|
3245
241838c01caf
Removal of redundant code (unused or already present in Isabelle.
paulson
parents:
2112
diff
changeset
|
12 |
val eqT :thm |
241838c01caf
Removal of redundant code (unused or already present in Isabelle.
paulson
parents:
2112
diff
changeset
|
13 |
val rev_eq_mp :thm |
241838c01caf
Removal of redundant code (unused or already present in Isabelle.
paulson
parents:
2112
diff
changeset
|
14 |
val simp_thm :thm |
2112 | 15 |
end; |