isabelle: TFL/thms.sig@9935800edf58 (annotated)

3302 404fe31fd8d2 New headers and other minor changes paulson parents: 3245 diff changeset	1	(* Title: TFL/thms
404fe31fd8d2 New headers and other minor changes paulson parents: 3245 diff changeset	2	ID: $Id$
404fe31fd8d2 New headers and other minor changes paulson parents: 3245 diff changeset	3	Author: Konrad Slind, Cambridge University Computer Laboratory
404fe31fd8d2 New headers and other minor changes paulson parents: 3245 diff changeset	4	Copyright 1997 University of Cambridge
404fe31fd8d2 New headers and other minor changes paulson parents: 3245 diff changeset	5	*)
404fe31fd8d2 New headers and other minor changes paulson parents: 3245 diff changeset	6
2112 3902e9af752f Konrad Slind's TFL paulson parents: diff changeset	7	signature Thms_sig =
3902e9af752f Konrad Slind's TFL paulson parents: diff changeset	8	sig
3245 241838c01caf Removal of redundant code (unused or already present in Isabelle. paulson parents: 2112 diff changeset	9	val WF_INDUCTION_THM:thm
241838c01caf Removal of redundant code (unused or already present in Isabelle. paulson parents: 2112 diff changeset	10	val WFREC_COROLLARY :thm
241838c01caf Removal of redundant code (unused or already present in Isabelle. paulson parents: 2112 diff changeset	11	val CUT_DEF :thm
241838c01caf Removal of redundant code (unused or already present in Isabelle. paulson parents: 2112 diff changeset	12	val CUT_LEMMA :thm
241838c01caf Removal of redundant code (unused or already present in Isabelle. paulson parents: 2112 diff changeset	13	val SELECT_AX :thm
2112 3902e9af752f Konrad Slind's TFL paulson parents: diff changeset	14
3245 241838c01caf Removal of redundant code (unused or already present in Isabelle. paulson parents: 2112 diff changeset	15	val LET_CONG :thm
2112 3902e9af752f Konrad Slind's TFL paulson parents: diff changeset	16
3245 241838c01caf Removal of redundant code (unused or already present in Isabelle. paulson parents: 2112 diff changeset	17	val eqT :thm
241838c01caf Removal of redundant code (unused or already present in Isabelle. paulson parents: 2112 diff changeset	18	val rev_eq_mp :thm
241838c01caf Removal of redundant code (unused or already present in Isabelle. paulson parents: 2112 diff changeset	19	val simp_thm :thm
2112 3902e9af752f Konrad Slind's TFL paulson parents: diff changeset	20	end;

author	wenzelm
	Sat, 14 Nov 1998 13:25:34 +0100
changeset 5863	9935800edf58
parent 3458	5ff4bfab859c
child 6498	1ebbe18fe236
permissions	-rw-r--r--