Mercurial Mercurial > repos > isabelle / annotate
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
TFL/thms.sig
author paulson
Thu, 08 Jul 1999 13:44:47 +0200
changeset 6918 63c9df6b5c4b
parent 6498 1ebbe18fe236
permissions -rw-r--r--
Now if_weak_cong is a standard congruence rule
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
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;















isabelle