author | paulson |
Wed, 18 Aug 1999 12:23:10 +0200 | |
changeset 7250 | a4bd83b25d23 |
parent 7249 | 4886664d7033 |
child 7251 | 35de2117b5dd |
TFL/rules.sig | file | annotate | diff | comparison | revisions |
--- a/TFL/rules.sig Wed Aug 18 11:49:46 1999 +0200 +++ b/TFL/rules.sig Wed Aug 18 12:23:10 1999 +0200 @@ -45,9 +45,11 @@ val EVEN_ORS : thm list -> thm list val DISJ_CASESL : thm -> thm list -> thm + val list_beta_conv : cterm -> cterm list -> thm val SUBS : thm list -> thm -> thm val simpl_conv : simpset -> thm list -> cterm -> thm + val rbeta : thm -> thm (* For debugging my isabelle solver in the conditional rewriter *) val term_ref : term list ref val thm_ref : thm list ref