TFL/rules.sig
changeset 7262 a05dc63ca29b
parent 7260 745f834281e2
--- 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