Mercurial Mercurial > hg > nominal2 / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
deleted two functions from the API
authorChristian Urban <urbanc@in.tum.de>
Tue, 03 May 2011 13:25:02 +0100
changeset 2778 d7183105e304
parent 2777 75a95431cd8b
child 2779 3c769bf10e63
deleted two functions from the API
Nominal/nominal_eqvt.ML file | annotate | diff | comparison | revisions 
--- 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
nominal2