new version from Konrad with "lazy" (deferred) definitons

--- 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