# HG changeset patch
# User berghofe
# Date 934991033 -7200
# Node ID 745f834281e2428ca3c1a6c0368623273ea690de
# Parent  e75aa311788c79ea9e4c653e5492188f10705ceb
Removed rbeta.

diff -r e75aa311788c -r 745f834281e2 TFL/rules.sig
--- a/TFL/rules.sig	Wed Aug 18 17:31:53 1999 +0200
+++ b/TFL/rules.sig	Wed Aug 18 17:43:53 1999 +0200
@@ -49,7 +49,6 @@
   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