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

author	paulson
	Tue, 27 May 1997 13:22:30 +0200
changeset 3353	9112a2efb9a3
parent 3302	404fe31fd8d2
child 3458	5ff4bfab859c
permissions	-rw-r--r--