# HG changeset patch
# User urbanc
# Date 1156880614 -7200
# Node ID eef4e9081beabd817bd96938afde8e349f914d2c
# Parent  fd646e926983b18b31c040cc8b62e16d585d1f41
added a FIXME-comment

diff -r fd646e926983 -r eef4e9081bea src/HOL/Nominal/nominal_permeq.ML
--- a/src/HOL/Nominal/nominal_permeq.ML	Tue Aug 29 18:56:11 2006 +0200
+++ b/src/HOL/Nominal/nominal_permeq.ML	Tue Aug 29 21:43:34 2006 +0200
@@ -6,6 +6,25 @@
 for analysing equations involving permutations.
 *)
 
+(*
+FIXMES:
+
+ - allow the user to give an explicit set S in the
+   fresh_guess tactic which is then verified
+
+ - the perm_compose tactic does not do an "outermost
+   rewriting" and can therefore not deal with goals
+   like
+
+      [(a,b)] o pi1 o pi2 = ....
+
+   rather it tries to permute pi1 over pi2, which 
+   results in a failure when used with the 
+   perm_(full)_simp tactics
+
+*)
+
+
 signature NOMINAL_PERMEQ =
 sig
   val perm_simp_tac : simpset -> int -> tactic