diff -r a141985d660b -r a05dc63ca29b TFL/rules.sig --- a/TFL/rules.sig Wed Aug 18 18:10:48 1999 +0200 +++ b/TFL/rules.sig Wed Aug 18 18:44:20 1999 +0200 @@ -49,6 +49,7 @@ 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