Mercurial Mercurial > hg > nominal2 / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Nominal/nominal_permeq.ML
changeset 3183 313e6f2cdd89
parent 2781 542ff50555f5
child 3229 b52e8651591f 
--- a/Nominal/nominal_permeq.ML	Thu May 31 12:01:13 2012 +0100
+++ b/Nominal/nominal_permeq.ML	Mon Jun 04 21:39:51 2012 +0100
@@ -18,6 +18,7 @@
   val delpres : eqvt_config -> eqvt_config
   val delposts : eqvt_config -> eqvt_config
 
+  val eqvt_conv: Proof.context -> eqvt_config -> conv 
   val eqvt_rule: Proof.context -> eqvt_config -> thm -> thm
   val eqvt_tac: Proof.context -> eqvt_config -> int -> tactic
nominal2