20060406 
urbanc 
20060406 
modified the perm_compose rule such that it
is applied as simplification rule (as simproc)
in the restricted case where the first
permutation is a swapping coming from a supports
problem
also deleted the perm_compose' rule from the set
of rules that are automatically tried

file  diff  annotate 
20060301 
urbanc 
20060301 
fixed a problem where a permutation is not analysed
when the term is of the form
(pi o f) x1...xn
This was the case because the head of this term is the
constant "nominal.perm". Now an applicability predicate
decides the right behaviour of the simproc

file  diff  annotate 
20060301 
urbanc 
20060301 
made some small tunings in the decisionprocedure
(in the order how the "small" tactics are called)

file  diff  annotate 
20060227 
urbanc 
20060227 
added a finite_guess tactic, which solves
automatically finitesupport goals

file  diff  annotate 
20060227 
urbanc 
20060227 
added support for arbitrary atoms in the simproc

file  diff  annotate 
20060226 
urbanc 
20060226 
improved the decisionprocedure for permutations;
now uses a simproc
FIXME:
the simproc still needs to be adapted for arbitrary
atom types

file  diff  annotate 
20051219 
urbanc 
20051219 
fixed a bug that occured when more than one atomtype
is declared.

file  diff  annotate 
20051129 
urbanc 
20051129 
made some of the theorem lookups static (by using
thm instead of PureThy.get_thm)

file  diff  annotate 
20051101 
urbanc 
20051101 
tunings of some comments (nothing serious)

file  diff  annotate 
20051029 
urbanc 
20051029 
Changed Simplifier.simp_modifiers to Simplifier.simp_modifiers'.
This means the syntax of the tactics supports_simp and perm_simp
are exactly like simp, namely
(supports_simp add: .... del: ...)
where the add's and del's are optional.

file  diff  annotate 
20051028 
urbanc 
20051028 
Added (optional) arguments to the tactics
perm_eq_simp and supports_simp. They now
follow the "simp"way and use the syntax:
apply(supports_simp simp add: thms)
etc.

file  diff  annotate 
20051017 
berghofe 
20051017 
Initial revision.

file  diff  annotate 