isabelle: TFL/thms.sig@d7e85fd09291 (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 SELECT_AX :thm
2112 3902e9af752f Konrad Slind's TFL paulson parents: diff changeset	13
3245 241838c01caf Removal of redundant code (unused or already present in Isabelle. paulson parents: 2112 diff changeset	14	val LET_CONG :thm
2112 3902e9af752f Konrad Slind's TFL paulson parents: diff changeset	15
3245 241838c01caf Removal of redundant code (unused or already present in Isabelle. paulson parents: 2112 diff changeset	16	val eqT :thm
241838c01caf Removal of redundant code (unused or already present in Isabelle. paulson parents: 2112 diff changeset	17	val rev_eq_mp :thm
241838c01caf Removal of redundant code (unused or already present in Isabelle. paulson parents: 2112 diff changeset	18	val simp_thm :thm
2112 3902e9af752f Konrad Slind's TFL paulson parents: diff changeset	19	end;

author	paulson
	Wed, 16 Feb 2000 10:50:57 +0100
changeset 8248	d7e85fd09291
parent 6498	1ebbe18fe236
permissions	-rw-r--r--