diff -r 4886664d7033 -r a4bd83b25d23 TFL/rules.sig --- 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