# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1304425502 -3600
# Node ID d7183105e304307706ea6b071702072d7acc2868
# Parent  75a95431cd8bdfbe00059a6441113fd68886e5d6
deleted two functions from the API

diff -r 75a95431cd8b -r d7183105e304 Nominal/nominal_eqvt.ML
--- a/Nominal/nominal_eqvt.ML	Tue May 03 13:09:08 2011 +0100
+++ b/Nominal/nominal_eqvt.ML	Tue May 03 13:25:02 2011 +0100
@@ -8,9 +8,6 @@
 
 signature NOMINAL_EQVT =
 sig
-  val eqvt_rel_tac: Proof.context -> string list -> term -> thm -> thm list -> int -> tactic
-  val eqvt_rel_single_case_tac: Proof.context -> string list -> term -> thm -> int -> tactic
-  
   val raw_equivariance: bool -> term list -> thm -> thm list -> Proof.context -> thm list * local_theory
   val equivariance: string -> Proof.context -> (thm list * local_theory)
   val equivariance_cmd: string -> Proof.context -> local_theory